\documentclass[10pt]{sigplanconf}


\conferenceinfo{OOPSLA/SPLASH'10,} {October 17--21, 2010, Reno/Tahoe, Nevada, USA.}
\CopyrightYear{2010}
\copyrightdata{978-1-4503-0203-6/10/10}


\usepackage{relsize}
\usepackage{amsmath}
\usepackage{url}


%
\usepackage{listings}


\usepackage[ruled]{algorithm} %
\usepackage[noend]{algorithmic} %
\renewcommand\algorithmiccomment[1]{// \textit{#1}} %


%
\usepackage{microtype}


%
\usepackage{pslatex}


\usepackage{xspace}
\usepackage{yglabels}
\usepackage{yglang}
\usepackage{ygequation}
\usepackage{graphicx}
%

\newcommand{\formalrule}[1]{\mbox{\textsc{\scriptsize #1}}}
\newcommand{\myrule}[1]{\textsc{\codesmaller #1 Rule}}
\newcommand{\umyrule}[1]{\textbf{\underline{\textsc{\codesmaller #1 Rule}}}}


%
%
%
%
\newcommand{\normalcode}[1]{\texttt{\textup{#1}}}
\def\codesmaller{\small}
\newcommand{\myCOMMENT}[1]{\COMMENT{\small #1}}
\newcommand{\code}[1]{\texttt{\textup{\codesmaller #1}}}
%
%
\newcommand{\smallcode}[1]{\texttt{\textup{\scriptsize #1}}}
%

%
\newcommand{\keyword}[1]{\code{#1}}

%
\newcommand{\hparen}[1]{\code{(}#1\code{)}}

\newcommand{\hgn}[1]{\lt#1\gt} %

\newcommand{\Own}{{\it O}}
\newcommand{\Ifn}[1]{\ensuremath{I(#1)}}
\newcommand{\Ofn}[1]{\ensuremath{O(#1)}}
\newcommand{\Cooker}[1]{\ensuremath{{\kappa}(#1)}}
\newcommand{\Owner}[1]{\ensuremath{{\theta}(#1)}}
\newcommand{\Oprec}[0]{\ensuremath{\preceq_{\theta}}}
\newcommand{\Tprec}[0]{\ensuremath{\preceq^T}}
\newcommand{\TprecNotEqual}[0]{\ensuremath{\prec^T}}
\newcommand{\OprecNotEqual}[0]{\ensuremath{\prec_{\theta}}}
\newcommand{\IfnDelta}[1]{\ensuremath{I_\Delta(#1)}}
\newcommand\Abs[1]{\ensuremath{\left\lvert#1\right\rvert}}
\newcommand{\erase}[1]{\ensuremath{\Abs{#1}}}

\newcommand{\CookerH}[1]{\ensuremath{{\kappa}_H(#1)}}
\newcommand{\IfnH}[1]{\ensuremath{I_H(#1)}}
\newcommand{\OwnerH}[1]{\ensuremath{{\theta}_H(#1)}}
\newcommand{\KGdash}[0]{\ensuremath{K,\Gamma \vdash }}
\newcommand{\reducesto}[0]{\rightarrow}

\usepackage{color}
\definecolor{light}{gray}{.75}


\newcommand{\todo}[1]{\textbf{[[#1]]}}
%
%

%
\newcommand{\TODO}[1]{\todo{TODO: #1}}

\newcommand\xX[1]{$\textsuperscript{\textit{\text{#1}}}$}


\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\nounderline}[1]{{#1}}


%
\newcommand{\typerule}[2]{
\begin{array}{c}
  #1 \\
\hline
  #2
\end{array}}


%
\newcommand{\inside}{\prec}
\newcommand{\visible}{{\it visible}}
\newcommand{\placeholderowners}{{\it placeholderowners}}
\newcommand{\nullexpression}{{\tt null}}
\newcommand{\errorexpression}{{\tt error}}
\newcommand{\locations}{{\it locations}} %
\newcommand{\xo}{{\tt X^O}}
\newcommand{\no}{{\tt N^O}}
\newcommand{\co}{{\tt C^O}}
\newcommand{\I}{\it I}


\newcommand\mynewcommand[2]{\newcommand{#1}{#2\xspace}}

\mynewcommand{\hA}{\code{A}} %
\mynewcommand{\hB}{\code{B}} %

\mynewcommand{\hI}{\code{I}} %

%
\mynewcommand{\hJ}{\code{J}}
\mynewcommand{\hO}{\code{O}}
\mynewcommand{\ho}{\code{o}}

\mynewcommand{\hX}{\code{X}} %
\mynewcommand{\hY}{\code{Y}} %
\mynewcommand{\hC}{\code{C}} %
\mynewcommand{\hc}{\code{c}} %
\mynewcommand{\hL}{\code{L}} %
\mynewcommand{\hM}{\code{M}} %
\mynewcommand{\hN}{\code{N}} %
\mynewcommand{\hm}{\code{m}} %
\mynewcommand{\he}{\code{e}} %
\mynewcommand{\hv}{\code{v}} %
\mynewcommand{\hl}{\code{l}} %
\mynewcommand{\lroot}{\code{l}_\top} %
\mynewcommand{\lthis}{\code{l}_\smallcode{this}} %
\mynewcommand{\hx}{\code{x}} %
\mynewcommand{\hf}{\code{f}} %
\mynewcommand{\hF}{\code{F}} %
\mynewcommand{\hT}{\code{T}} %
\mynewcommand{\hU}{\code{U}} %
\mynewcommand{\hV}{\code{V}} %
\mynewcommand{\hH}{\code{H}} %
\mynewcommand{\hS}{\code{S}}
\mynewcommand{\hsub}{\code{/}} %
\mynewcommand{\hthis}{\code{this}} %
\mynewcommand{\hclass}{\code{class}}
\mynewcommand{\hreturn}{\code{return}}
\mynewcommand{\hnew}{\code{new}}
\newcommand{\lt}{\code{<}}%
\newcommand{\gt}{\code{>}}%

\mynewcommand{\this}{\keyword{this}}
\mynewcommand{\Object}{\code{Object}}
\mynewcommand{\const}{\keyword{const}} %
\mynewcommand{\mutable}{\keyword{mutable}} %
\mynewcommand{\romaybe}{\keyword{romaybe}} %

%
%

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}


\mynewcommand{\IP}{\code{I}}   %
\mynewcommand{\JP}{\code{J}}   %


\mynewcommand{\Iparam}{Immutability parameter}
\mynewcommand{\iparam}{immutability parameter}
\mynewcommand{\iparams}{immutability parameters}
\mynewcommand{\Iparams}{Immutability parameters}
\mynewcommand{\Iarg}{Immutability argument}
\mynewcommand{\iarg}{immutability argument}
\mynewcommand{\iargs}{immutability arguments}
\mynewcommand{\Iargs}{Immutability arguments}
\mynewcommand{\ReadOnly}{\code{ReadOnly}}
\mynewcommand{\WriteOnly}{\code{WriteOnly}}
\mynewcommand{\None}{\code{None}}
\mynewcommand{\Mutable}{\code{Mutable}}
\mynewcommand{\Immut}{\code{Immut}}
\mynewcommand{\Raw}{\code{Raw}}


\mynewcommand{\This}{\code{This}}
\mynewcommand{\World}{\code{World}}


%
\mynewcommand{\OMutable}{\code{@OMutable}}
\mynewcommand{\OI}{\code{@OI}}


\mynewcommand{\InVariantAnnot}{\code{@InVariant}}


\newcommand{\func}[1]{\text{\textnormal{\textit{\codesmaller #1}}}}


\mynewcommand{\st}{\ensuremath{\mathrel{{\leq}}}} %
\mynewcommand{\notst}{\mathrel{\st\hspace{-1.5ex}\rule[-.25em]{.4pt}{1em}~}}
\mynewcommand{\tl}{\ensuremath{\triangleleft}}
\mynewcommand{\gap}{~ ~ ~ ~ ~ ~}


\newcommand{\RULE}[1]{\textsc{\scriptsize{}#1}} %


\mynewcommand{\DA}{\texttt{DA}}
\mynewcommand{\ok}{\texttt{OK}}
\mynewcommand{\subterm}{\func{subterm}}
\mynewcommand{\TP}{\func{TP}} %
\mynewcommand{\CT}{\func{CT}} %
\mynewcommand{\mtype}{\func{mtype}}
\mynewcommand{\mbody}{\func{mbody}}
\mynewcommand{\bound}{\func{bound}_\Delta}
\mynewcommand{\substitute}{\func{substitute}}
\mynewcommand{\fields}{\func{fields}}
\mynewcommand{\ftype}{\func{ftype}}
\mynewcommand{\mguard}{\func{mguard}}
\mynewcommand{\isTransitive}{\func{isTransitive}}
\DeclareMathOperator{\dom}{dom}


\mynewcommand\xth{\xX{th}}
\mynewcommand\xrd{\xX{rd}}
\mynewcommand\xnd{\xX{nd}}
\mynewcommand\xst{\xX{st}}
\mynewcommand\ith{$i$\xth}
\mynewcommand\jth{$j$\xth}


%
\mynewcommand{\myindent}{~~}


%
\makeatletter
\def\topfigrule{\kern3\p@ \hrule \kern -3.4\p@} %
\def\botfigrule{\kern-3\p@ \hrule \kern 2.6\p@} %
\def\dblfigrule{\kern3\p@ \hrule \kern -3.4\p@} %
\makeatother

\setlength{\textfloatsep}{.75\textfloatsep}


%
%
\makeatletter
%
\makeatother


%
\usepackage{bold-extra}


%
\newcommand{\ttlcb}{\texttt{\char "7B}}
\newcommand{\ttrcb}{\texttt{\char "7D}}
\newcommand{\lb}{\ttlcb}
\newcommand{\rb}{\ttrcb}


\setlength{\leftmargini}{.75\leftmargini}



\begin{document}


\lstset{language=java,basicstyle=\ttfamily\small}


\title{Ownership and Immutability in Generic Java}

%
\makeatletter
\def \@titleauthors #1#2#3{%
    \noindent \@setauthor{16.5pc}{#1}{\@false}\hspace{1pc}%
              \@setauthor{12pc}{#2}{\@false}\hspace{1pc}%
              \@setauthor{11pc}{#3}{\@true}\par
  \vspace{10pt}}
\makeatother


\authorinfo{Yoav Zibin \and Alex Potanin \and Paley Li}
           {Victoria University of Wellington \\ Wellington, New Zealand}
           {yoav$|$alex$|$lipale@ecs.vuw.ac.nz}
\authorinfo{Mahmood Ali}
           {\mbox{Massachusetts Institute of Technology} \\ Cambridge, MA, USA}
           {mali@csail.mit.edu}
\authorinfo{Michael D.~Ernst}
           {University of Washington \\ Seattle, WA, USA}
           {mernst@cs.washington.edu}


\maketitle


\begin{abstract}
The Java language lacks the important notions of
    \emph{ownership} (an object owns its representation to prevent unwanted
    aliasing)
    and \emph{immutability} (the division into mutable, immutable, and
    readonly data and references).
Programmers are prone to design errors,
    such as representation exposure or violation of immutability contracts.
This paper presents \emph{Ownership Immutability Generic Java} (OIGJ),
    a backward-compatible purely-static language extension supporting
    ownership and immutability.
We formally defined a core calculus for OIGJ, based on Featherweight Java, and proved it sound.
We also implemented OIGJ and performed case studies on 33,000 lines of code.

Creation of immutable cyclic structures requires a ``\emph{cooking phase}'' in which
    the structure is mutated but the outside world cannot observe this mutation.
OIGJ uses \emph{ownership} information to facilitate creation of \emph{immutable} cyclic structures,
    by safely prolonging the cooking phase even after the constructor finishes.

%
%
%
%
%
%
%

OIGJ is easy for a programmer to use,
    and it is easy to implement
    (flow-insensitive, adding only 14 rules to those of Java).
Yet, OIGJ is more expressive than previous ownership languages,
    in the sense that it can type-check more good code.
OIGJ can express the factory and visitor patterns, and
OIGJ can type-check
    Sun's \code{java.util} collections (except for the \code{clone} method)
    without refactoring and with only a small number of annotations.
Previous work required major refactoring of existing code in
    order to fit its ownership restrictions.
Forcing refactoring of well-designed code is undesirable
    because it costs programmer effort,
    degrades the design,
    and hinders adoption in the mainstream community.

%
%

\label{dummy-label-for-etags}

%

\end{abstract}

\category{D.3.3}{Programming Languages}{Language Constructs and Features}
\category{D.1.5}{Programming Techniques}{Object-oriented Programming}

\terms
Experimentation, Languages, Theory

%
%
%


\Section[introduction]{Introduction}
%
%
%
%
%
%

%
%
%
%
%
%
%
%
%
%

This paper presents \emph{Ownership Immutability Generic Java} (OIGJ),
    a simple and practical language extension
    that expresses both ownership and immutability information.
OIGJ is purely static, without any run-time representation.
This enables executing the resulting code on any JVM without run-time penalty.
Our ideas, though demonstrated using Java,
    are applicable to any statically typed language with generics,
    such as \CC, C\#, Scala, and Eiffel.

OIGJ follows the \emph{owner-as-dominator}
    discipline~\cite{Boyapati2004:PhD,ClarkeD2002,PotaninNCB2006}
    where an object cannot leak beyond its owner:
    outside objects cannot access it.
If an object owns
    its representation, then there are no aliases to its
    internal state.
For example, a \code{LinkedList} should own all its \code{Entry} objects
    (but not its elements); entries should not be exposed to clients, and
    entries from different lists must not be mixed.

The keyword \code{private} does not offer
    such strong protection as ownership, because
    a careless programmer might write a public method
    that exposes a private object (a.k.a.\ representation exposure).
Phrased differently, the name-based protection used in Java
    hides the variable but not the object,
    as opposed to ownership that ensures proper encapsulation.
The key idea in ownership is that representation objects
    are nested and encapsulated inside the objects to which they belong.
Because this nesting is transitive, this kind of ownership is also called
    \emph{deep} ownership~\cite{ClarkeW2003:ECOOP}.

OIGJ is based on our previous type systems for ownership (OGJ~\cite{PotaninNCB2006})
    and immutability (IGJ~\cite{ZibinPAAKE2007}).
Although ownership and immutability may seem like two unrelated concepts,
    a design involving both enhances
    the expressiveness of each individual concept.
On the one hand,
    immutability previously enhanced ownership by relaxing
    owner-as-dominator to owner-as-modifier~\cite{MuellerPoetzsch-Heffter99a}:
    it constrains modification instead of aliasing.
On the other hand, the benefits of adding ownership
    on top of immutability have not been investigated before.
One such benefit is easier creation of immutable cyclic data-structures
    by using ownership information.

Constructing an immutable object must be done with care.
An object begins in the \emph{raw} (not fully initialized) state and transitions to the \emph{cooked} state~\cite{BoylandRZ2009}
    when initialization is complete.
For an immutable object,
field assignment is allowed only when the object is \emph{raw},
    i.e., the object cannot be modified after it is \emph{cooked}.
An immutable object should not be visible to the outside world in its raw state
    because it would seem to be mutating.
%
The challenge in building an immutable cyclic data-structure is that
    many objects must be raw simultaneously to create the cyclic structure.
Previous work restricted cooking an object to the constructor,
    i.e., an object becomes cooked when \underline{its} constructor finishes.

Our key observation is that
    \emph{an object can be cooked when \underline{its owner's} constructor finishes}.
More precisely, in OIGJ, a programmer can choose between cooking
    an object until its constructor finishes,
    or until its owner becomes cooked.
Because the object is encapsulated within its owner, the outside world
    will not see this cooking phase.
By adding ownership information, we can prolong the cooking time
    to make it easier to create complex data-structures.

Consider building an immutable \code{LinkedList} %
    (Sun's implementation is similar): %
    %

\begin{algorithmic}
\STATE \code{LinkedList(Collection<E> c)}
\STATE \code{\lb~this();}
\STATE \code{~~Entry<E> succ = this.header, pred = succ.prev;} %
\STATE \code{~~for (E e : c)}
\STATE \code{~~\lb~Entry<E> entry = new Entry<E>(e,succ,pred);}
\STATE \code{~~~~}\myCOMMENT{It is illegal to change an entry after it is cooked.}
\STATE \code{~~~~pred\underline{.next =} entry;~~pred = entry; \rb}
%
\STATE \code{~~succ\underline{.prev =} pred;~\rb}
%
\end{algorithmic}
An immutable list contains immutable entries, i.e.,
    the fields \code{next} and \code{prev} cannot be changed after an entry is cooked.
In IGJ and previous work on immutability, %
    an object becomes cooked
    after \underline{its} constructor finishes.
Because \code{next} and \code{prev} are changed after that time,
    this code is illegal.
In contrast, in OIGJ, this code type-checks if we specify that
    the list (the \this object) owns all its entries (the entries are the list's representation).
The entries will become cooked when \underline{their owner's} (the list's) constructor finishes,
    thus permitting the underlined assignments during the list's construction.
%
Therefore, there was no need to refactor the constructor of
    \code{LinkedList} for the benefit of OIGJ type-checking.

%
%
%
%
%
%
%

%
%
%
%

%
%
%
%
%


Informally, OIGJ provides the following ownership and immutability guarantees.
Let~$\Owner{o}$ denote the owner of~$o$ and let~$\Oprec$ denote the ownership tree,
    i.e.,
    the transitive, reflexive closure of~$o \Oprec \Owner{o}$.
Phrased differently, $\Owner{o}$ is the parent of $o$ in the tree,
    and the top (biggest) node in the tree is the root \World.
We say that $o_1$ is \emph{inside} $o_2$ iff $o_1 \Oprec o_2$,
    and it is \emph{strictly inside} if  $o_1 \neq o_2$.

%

\textbf{Ownership guarantee:}
    An object~$o'$ can point to object~$o$ iff~$o' \Oprec \Owner{o}$,
%
        i.e.,~$o$ is owned by~$o'$ or by one of its owners.
(This is the classical guarantee of \emph{owner-as-dominator}.) %

\textbf{Immutability guarantee:}
    An immutable object cannot be changed after it is cooked.
(When exactly an object becomes cooked is formally defined in \Ref{Section}{formal}.)
%


\paragraph{Contributions}
The main contributions of this paper are:
\begin{description}
  \item[Simplify ownership mechanisms]
    Most previous works used new mechanisms that are orthogonal to generics.
    Our previous work (OGJ and IGJ) reuses Java's underlying generic mechanism.
    However, OGJ prohibited using generic wildcards and certain kinds of generic methods.
    OIGJ increases the expressiveness of OGJ without introducing new mechanisms,
        by implementing
        scoped regions~\cite{Wrigstad2006} using \emph{generic methods},
        and existential owners~\cite{WrigstadC2007} using \emph{generic wildcards}.

  \item[No refactoring of existing code] %
    Java's collection classes (\code{java.util}) are properly encapsulated.
    We have implemented OIGJ,
        and verified the encapsulation by running the OIGJ type-checker
        without changing the source code (except for the \code{clone} method).
    Verifying Sun's \code{LinkedList} requires only 3 ownership annotations
        (see \Ref{Section}{case-studies}).
    Previous approaches to ownership or
        immutability required major refactoring of this codebase.

%
%
%
%

  \item[Flexibility]
    As illustrated by our case study, OIGJ is more flexible and practical
    than previous type systems.  For example, OIGJ can type-check the
    visitor design pattern
    %
    (see \Ref{Section}{oigj-language}), but other \emph{ownership}
    languages cannot~\cite{Nageli2006}. %
    Another advantage of OIGJ %
        is that
        it uses ownership information to facilitate creating immutable cyclic structures
        by prolonging their cooking phase.

  \item[Formalization]
    We define a Featherweight OIGJ (FOIGJ) calculus to
        formalize the concepts of raw/cooked objects and wildcards as owner parameters.
    We prove FOIGJ is sound and show our ownership and immutability guarantees.

\end{description}


\textbf{Outline.} %
\Ref{Section}{oigj-language}
        presents the OIGJ\@ language.
        %
        %
\Ref{Section}{formal} defines the OIGJ formalization.
\Ref{Section}{case-studies} discusses the OIGJ implementation and the collections case study.
\Ref{Section}{related-work} compares OIGJ to related work,
    and \Ref{Section}{conclusion} concludes.

%



\Section[oigj-language]{OIGJ Language}
This section presents the OIGJ language extension
    that expresses both ownership and immutability information.
We first describe the OIGJ syntax (\Ref{Section}{oigj-syntax}).
We then proceed with a \code{LinkedList} class example (\Ref{Section}{LinkedList}),
    followed by the OIGJ typing rules (\Ref{Section}{typing-rules}).
We conclude with the
    factory (\Ref{Section}{Factory})
    and visitor (\Ref{Section}{Visitor}) design patterns in OIGJ.


\Subsection[oigj-syntax]{OIGJ syntax}
OIGJ introduces two new type parameters to each type,
    called the \emph{owner parameter} and the
    \emph{immutability parameter}.
For simplicity of presentation, in the rest of this paper we assume that the special
    type parameters are at the beginning of the list of type parameters.
We stress that generics in Java are erased during compilation to bytecode
    and do not exist at run time,
    therefore OIGJ does not incur any run-time overhead (nor does it support run-time casts).

In OIGJ, all classes are subtypes of the parameterized root type \code{Object<\underline{O,I}>}
    that declares an owner and an immutability parameter.
In \underline{O}\underline{I}GJ,
    the first parameter is the owner (\underline{O}),
    and the second is the immutability (\underline{I}).
All subclasses must invariantly preserve
    their owner and immutability parameter.
The owner and immutability parameters form two separate hierarchies,
    which are shown in \Ref{Figure}{owners-and-immutability-params}.
These parameters cannot be extended, and they have no subtype relation with any other types.
%
%
The subtyping relation is denoted by~\st, e.g.,
$\Mutable\st\ReadOnly$.
Subtyping is invariant in the owner parameter and covariant in the immutability parameter.
    (See also paragraph \textbf{\emph{Subtype relation}} in \Ref{Section}{typing-rules}.)

%
%
%

Note that the \emph{owner parameter} \code{O} is a \emph{type},
    whereas the \emph{owner} of an object is an \emph{object}.
For example, if the owner parameter is \This,
    then the owner is the object \this.
Therefore, the owner parameter (which is a type) at compile time
    corresponds to an owner (which is an object) at run time.
    (See also paragraph \textbf{\emph{Owner vs.\ Owner-parameter}} below.)

OIGJ syntax borrows from
    \emph{conditional Java} (cJ)~\cite{HuangZS2007:cJ},
    where a programmer can write method \emph{guards}.
A guard of the form~\code{\underline{<X extends Y>?} METHOD\_DECLARATION}
    has a dual meaning:
    (i)~the method is applicable only if the type argument that substitutes~\code{X} extends~\code{Y},
    and (ii)~the bound of \code{X} inside \code{METHOD\_DECLARATION} changes to \code{Y}.
The guards are used to express the immutability of \this:  a method
    receiver or a constructor result.  For example,
    a method guarded with \code{\underline{<I extends Mutable>?}} means
    that (i)~the method is applicable only if the receiver is mutable
    and therefore (ii)~\this can be mutated inside the method.

\begin{figure}[t]
\centering
\includegraphics[scale=0.75]{owners-and-immutability-params}
\caption{The type hierarchy of (a) ownership and (b) immutability parameters.
    \World means the entire world can access the object,
        whereas \This means that \this owns the object and no one else can access it.
    The meaning of \Mutable/\Immut is obvious.
%
    A \ReadOnly reference points to a mutable or immutable object,
        and therefore cannot be used to mutate the object.
    \Raw represents an object under construction whose fields can be assigned.
    }
\label{Figure:owners-and-immutability-params}
\end{figure}




\begin{figure}[t]
\begin{algorithmic}[1]
\STATE \hspace{-1ex}\code{class Foo<\underline{O extends \World,I extends \ReadOnly{}}> \lb} \label{OIGJEx:decl}
\STATE \myCOMMENT{An immutable reference to an immutable date.}
\\ \code{Date\hgn{O,\underline{\Immut}} imD = new Date\hgn{O,\underline{\Immut}}();} \label{syntax:imD}
\STATE \myCOMMENT{A mutable reference to a mutable date.}
\\ \code{Date\hgn{O,\underline{\Mutable}} mutD = new Date\hgn{O,\underline{\Mutable}}();} \label{syntax:mutD}
\STATE \myCOMMENT{A readonly reference to any date.
    Both \code{roD} and \code{imD} cannot mutate their referent,
    however the referent of \code{roD} might be mutated by an alias,
    whereas the referent of \code{imD} is immutable.}
\\ \code{Date\hgn{O,\underline{\ReadOnly}} roD = \ldots\ ?\ imD : mutD; } \label{syntax:roD}
\STATE \myCOMMENT{A date with the same owner and immutability as \this.}
\\ \code{Date\hgn{\underline{O},\underline{I}} sameD;} \label{syntax:sameD}
\STATE \myCOMMENT{A date owned by \this; it cannot leak.}
\\ \code{Date\hgn{\underline{\This},I} ownedD;} \label{syntax:ownedD}
\STATE \myCOMMENT{Anyone can access this date.}
\\ \code{Date\hgn{\underline{\World},I} publicD;} \label{syntax:publicD}
\STATE \myCOMMENT{Can be called on any receiver; cannot mutate \this. The method guard ``\code{<\ldots>\underline{?}}" is part of cJ's syntax~\cite{HuangZS2007:cJ}.}
\\ \code{\underline{<I extends ReadOnly>?} int readonlyMethod() \lb\ldots{}\rb} \label{OIGJEx:cj:ro}
\STATE \myCOMMENT{Can be called only on mutable receivers; can mutate \this.}
\\ \code{\underline{<I extends Mutable>?} void mutatingMethod() \lb\ldots{}\rb} \label{OIGJEx:cj:mut}
\STATE \myCOMMENT{Constructor that can create (im)mutable objects.}
\\ \code{\underline{<I extends Raw>?} Foo(Date\hgn{\underline{O},I} d) \lb} \label{OIGJEx:cj:raw}
\STATE \code{~~this.sameD = d;} \label{OIGJEx:raw:sameD}
\STATE \code{~~\underline{this}.ownedD = new Date\hgn{\underline{This},I}();} \label{OIGJEx:raw:ownedD}
\STATE \code{~~}\myCOMMENT{Illegal, because \code{sameD} came from the outside.}
\\ \code{~~}\myCOMMENT{}\code{this.sameD.setTime(\ldots);} \label{OIGJEx:sameD:setTime}
\STATE \code{~~}\myCOMMENT{OK, because \Raw{} is transitive for owned fields.}
\\ \code{~~this.ownedD.setTime(\ldots);} \label{OIGJEx:ownedD:setTime}
\STATE \hspace{-1ex}\code{\rb}\code{\rb} \label{OIGJEx:cj:raw:end}
\end{algorithmic}
\caption{An example of OIGJ syntax.}
\label{Figure:OIGJ-example}
\end{figure}

\paragraph{Class definition example}
\Ref{Figure}{OIGJ-example} shows an example of OIGJ syntax.
A class definition declares
    the owner and immutability parameters (line~\ref{OIGJEx:decl});
    by convention we always denote them by \code{O} and~\code{I}
    and they always extend \World{} and \ReadOnly{}.
If the \code{extends} clause is missing from a class declaration,
    then we assume it extends \code{Object<O,I>}.

\paragraph{Immutability example}
Lines~\ref{syntax:imD}--\ref{syntax:roD} show different kinds of immutability in OIGJ:
    immutable, mutable, and readonly.
A readonly and an immutable reference may seem similar because neither
    can be used to mutate the referent.
However, line~\ref{syntax:roD} shows the difference between the two:
    a readonly reference may point to a mutable object.
Phrased differently, a readonly reference may not mutate its referent,
    though the referent may be changed via an aliasing mutable reference.

Java's type arguments are invariant (neither covariant nor contravariant), to avoid a type
    loophole~\cite{Igarashi:2001:FJM}, so line~\ref{syntax:roD} is
    illegal in Java.
Line~\ref{syntax:roD} is legal in OIGJ, because OIGJ safely allows covariant
    changes in the immutability parameter (but not in the owner parameter).
OIGJ \textit{restricts} Java by having additional typing rules, while at the same time
OIGJ also \textit{relaxes} Java's subtyping relation.
Therefore, neither OIGJ nor Java subsumes the other, i.e.,
    a legal OIGJ program may be illegal in Java (and vice versa).
However, because generics are erased during compilation, the resulting
    bytecode can be executed on any JVM.

The immutability of \code{sameD} (line~\ref{syntax:sameD}) depends on the immutability of \this,
    i.e., \code{sameD} is (im)mutable in an (im)mutable \code{Foo} object.
Similarly, the owner of \code{sameD} is the same as the owner of \this.



\paragraph{Ownership example}
Lines~\ref{syntax:sameD}--\ref{syntax:publicD} show three different owner parameters:
    \hO, \This, and \World.
The owner parameter is invariant, i.e., the subtype relation preserves the owner parameter.
For instance, the types on lines~\ref{syntax:sameD}--\ref{syntax:publicD}
    have no subtype relation with each other because they have different owner parameters.

Reference \code{ownedD} cannot leak outside of \this,
    whereas references \code{sameD} and \code{publicD}
    can potentially be accessed by anyone with access to \this.
Although \code{sameD} and \code{publicD} can be accessed by the same objects,
    they cannot be stored in the same places:
%
    \code{publicD} can be stored anywhere on the heap (even in a static public variable)
    whereas \code{sameD} can only be stored inside its owner.


We use \Ofn{\ldots} to denote the function that takes a type or a reference, and returns
    its owner parameter;
    e.g.,~$\Ofn{\code{ownedD}}=\This$.
Similarly, function \Ifn{\ldots} returns
    the immutability parameter;
    e.g.,~$\Ifn{\code{ownedD}}=\hI$.
We say that an object~\code{o} is \emph{\this-owned} (i.e., owned by \this)
    if~$\Ofn{\code{o}}=\This$;
    e.g., \code{ownedD} is \this-owned,
    but \code{sameD} is not.
OIGJ prevents leaking \this-owned objects by requiring
    that \this-owned fields (and methods with \this-owned arguments or return-type)
    can only be used via \this.
For example, \code{this.ownedD} is legal, but \code{foo.ownedD} is illegal.


\paragraph{Owner vs.\ owner-parameter}
Now we explain the connection between the \emph{owner parameter}~$\Ofn{o}$,
        which is a generic type parameter at \emph{compile time},
    and the \emph{owner}~$\Owner{o}$,
        which is an object at \emph{run time}.
\This is an owner parameter that represents an owner that is the current
  \this object, and
  \World represents the root of the ownership tree
  (we treat \World both as a type parameter and as an object that is the root of the ownership tree).
Formally, if $\Ofn{o}=\This$ then $\Owner{o}=\this$,
    if $\Ofn{o}=\hO$ then $\Owner{o}=\Owner{\this}$,
    and if $\Ofn{o}=\World$ then $\Owner{o}=\World$.
Two references (in the same class) with the same owner parameter (at compile time)
    will point to objects
    with the same owner (at run time),
    i.e., $\Ofn{o_1}=\Ofn{o_2}$ implies $\Owner{o_1}=\Owner{o_2}$.

Finally, recall the \textbf{Ownership guarantee}:~$o'$ can point to~$o$ iff~$o' \Oprec \Owner{o}$.
By definition of \Oprec, we have that for all~$o$:
    (i)~$o \Oprec o$, (ii)~$o \Oprec \Owner{o}$, and (iii)~$o \Oprec \World$.
By part (iii), if~$\Owner{o}=\World$ then anyone can point to~$o$.
On lines~\ref{syntax:sameD}--\ref{syntax:publicD}, we see that \this
    can point to \code{ownedD}, \code{sameD}, \code{publicD},
    whose owner parameters are~\This, \hO, \World,
    and whose owners are $\this$, $\Owner{\this}$, \World.
This conforms with the ownership guarantee according to parts (i), (ii), and~(iii), respectively.
%
More complicated pointing patterns can occur by using multiple owner parameters,
    e.g., an entry in a list can point to an element owned by the list's owner,
    such as in
    \code{List<\underline{This},I,Date<\underline{O},I>>}.

There is a similar connection between the immutability type parameter (at compile time)
    and the object's immutability (at run time).
Immutability parameter \Mutable or \Immut implies the object is mutable or immutable (respectively),
    \ReadOnly implies the referenced object may be either mutable or
    immutable and thus the object cannot be mutated through the read-only
    reference.
\Raw implies the object is still raw and thus can still be mutated,
        but it might become immutable after it is cooked.


\paragraph{Method guard example}
%
Lines~\ref{OIGJEx:cj:ro}~and~\ref{OIGJEx:cj:mut} show a readonly and a mutating method.
These methods are \emph{guarded} with \code{<\ldots>?}.
Conditional Java (cJ)~\cite{HuangZS2007:cJ} extends Java with such guards (a.k.a.~conditional type expressions).
Note that cJ changed Java's syntax by using the question mark in
    the guard \code{<\ldots>\underline{?}}.
The exposition in this paper uses cJ for convenience.
However, our implementation of OIGJ (\Ref{Section}{case-studies}) uses type annotations~\cite{JSR308-2008-09-12}
    without changing Java's syntax,
    for conciseness and compatibility with existing tools and code bases.

A guard such as \code{<T extends U>? METHOD\_DECLARATION} has a dual purpose:
    (i)~the method is included only if \code{T extends U},
    and (ii)~the bound of \code{T} is \code{U} inside the method.
In our example, the guard on line~\ref{OIGJEx:cj:mut}
    means that (i)~this method can only be called
        on a \Mutable receiver, and
        (ii)~inside the method the bound of \code{I} changes to \Mutable.
For instance,
    (i)~only a mutable \code{Foo} object can be a receiver of \code{mutatingMethod}, and
    (ii)~field~\code{sameD} is mutable in \code{mutatingMethod}.
cJ also ensures that the condition of an overriding method is
    equivalent or weaker than the condition of the overridden method.


IGJ~\cite{ZibinPAAKE2007} used \emph{declaration annotations} to denote
    the immutability of \this.
In this paper, OIGJ uses cJ to reduce the number of typing rules
    and handle inner classes more flexibly.\footnote{%
      Our implementation uses \emph{type annotations} to denote
      immutability of \this.  A type annotation \code{@Mutable} on the
      receiver is similar to a cJ \code{<I extends
        Mutable>?} construct, but it separates the distinct roles of the
      receiver and the result in inner class constructors.}
OIGJ does not use the full power of cJ:
    it only uses guards with immutability parameters.
Moreover, we modified cJ to treat guards over constructors
    in a special way described in the \textbf{Object creation rule} of \Ref{Figure}{oigj-typing-rules}.

To summarize, on lines~\ref{OIGJEx:cj:ro}--\ref{OIGJEx:cj:raw}
    we see three guards that change the bound of
    \code{I} to \ReadOnly, \Mutable, and \Raw, respectively.
Because the bound of \code{I} is already declared on line~\ref{OIGJEx:decl} as \ReadOnly{},
    the guard on line~\ref{OIGJEx:cj:ro} can be removed. %


\paragraph{Constructor example}
The constructor on line~\ref{OIGJEx:cj:raw} is guarded with \Raw,
    and therefore can create both mutable and immutable objects, because
    all objects start their life cycle as raw.
This constructor illustrates
    the interplay between \emph{ownership} and \emph{immutability},
    which makes OIGJ more expressive than previous work on immutability.
OIGJ uses ownership information to prolong the \emph{cooking phase} for owned objects:
    the cooking phase
    of \this-owned fields (\code{ownedD}) is longer than that of non-owned fields (\code{sameD}).
This property is critical to type-check the collection classes,
    as \Ref{Section}{LinkedList} will show.

Consider the following code:
%
\begin{algorithmic}
\STATE \code{class Bar<\underline{O extends \World,I extends \ReadOnly{}}>}
\STATE \code{~~\lb~Date<O,Immut> d = new Date<O,Immut>();}
\STATE \code{~~~~Foo<O,Immut> foo = new Foo<O,Immut>(d);~\rb}
%
\end{algorithmic}
Recall our \textbf{Immutability guarantee}:
    an immutable object cannot be changed after it is \emph{cooked}.
A \This-owned object is cooked
    when its owner is cooked (e.g., \code{foo.ownedD}).
Any other object is cooked
    when its constructor finishes (e.g., \code{d} and \code{foo}).
The intuition is that \code{ownedD} cannot leak and so the outside world
    cannot observe this longer cooking phase,
    whereas \code{d} is visible to the world after its constructor finishes and must not be mutated further.
The constructor on lines~\ref{OIGJEx:cj:raw}--\ref{OIGJEx:cj:raw:end} shows
    this difference between the assignments to \code{sameD} (line~\ref{OIGJEx:raw:sameD})
    and to \code{ownedD} (line~\ref{OIGJEx:raw:ownedD}):
    \code{sameD} can come from the outside world,
    whereas \code{ownedD} must be created inside \this.
Thus, \code{sameD} cannot be further mutated (line~\ref{OIGJEx:sameD:setTime})
    whereas \code{ownedD} can be mutated (line~\ref{OIGJEx:ownedD:setTime}) until its owner is cooked.

An object in a raw method, whose immutability parameter is \hI,
    is still considered raw (thus the modified body can still assign to its fields or call other raw methods)
    iff the object is \this or \this-owned.
Informally, we say that \Raw is \emph{transitive} only for \this or \this-owned objects.
For example, the receiver of the method call \code{sameD.setTime(\ldots)} is not \this nor \this-owned,
    and therefore the call on line~\ref{OIGJEx:sameD:setTime} is illegal;
    however, the receiver of \code{ownedD.setTime(\ldots)} is \this-owned,
    and therefore the call on line~\ref{OIGJEx:ownedD:setTime} is legal.
%
%



\Subsection[LinkedList]{\normalcode{LinkedList} example}

\Ref{Figure}{OIGJ-LinkedList} shows an implementation of \code{LinkedList} in OIGJ
    that is similar in spirit to Sun's implementation.
%
%
%
%
We explain this example in three stages:
    (i)~we first explain the data-structure, i.e.,
        the fields of a list and its entries (lines~\ref{Entry:start}--\ref{OIGJ:header}),
    (ii)~then we discuss the \Raw{} constructors that enable creation of
        immutable lists (lines~\ref{OIGJ:Raw:ctor1}--\ref{OIGJ:Raw:end}),
        and
    (iii)~finally we dive into the complexities of inner classes and iterators
        (lines~\ref{OIGJ:iterator}--\ref{I:Iterator:end}).


\paragraph{LinkedList data-structure}
A linked list has a header field (line~\ref{OIGJ:header})
    pointing to the first entry.
Each entry has an \code{element} and
    pointers to the \code{next} and \code{prev} entries (line~\ref{Entry:next}).
We explain first the immutability and then the ownership of each field.

Recall that we implicitly assume that \code{O} extends \World and that
    \code{*I} extends \ReadOnly
    on lines~\ref{Entry:start},~\ref{OIGJ:LinkedList},~\ref{ListItr:start} and~\ref{I:Iterator}.

An (im)mutable list contains (im)mutable entries,
    i.e., the entire data-structure is either mutable or immutable as a whole.
Hence, all the fields have the same immutability \code{I}.
The underlying generic type system propagates the immutability information
    without the need for special typing rules.

Next consider the ownership of the fields of \code{LinkedList} and \code{Entry}.
\This on line~\ref{OIGJ:header} expresses that the
    reference \code{header} points to an \code{Entry} owned by \this,
    i.e., the entry is encapsulated and
    cannot be aliased outside of \this.
\code{O} on line~\ref{Entry:next} expresses that
    the owner of \code{next} is the same as the owner of the entry,
    i.e., a linked-list owns \emph{all} its entries.
Note how the generics mechanism propagates the owner parameter,
    e.g., the type of \code{this.header.next.next} is \code{Entry<\underline{This},I,E>}.
Thus, the owner of all entries is the \this object, i.e., the list.

Finally, note that the field \code{element} has no immutability nor owner parameters,
    because they will be specified by the client that instantiates the list type,
    e.g., \\
    \code{LinkedList<This,Mutable,Date<\underline{World,ReadOnly}>>}

\begin{figure}
\begin{algorithmic}[1]
\STATE \code{class Entry<\underline{O,I},E> \lb} \label{Entry:start}
\STATE \code{~~E element;}
\STATE \code{~~Entry<\underline{O,I},E> next, prev;} \label{Entry:next}
\STATE \code{\rb} \label{Entry:end}
\STATE \code{class LinkedList<\underline{O,I},E> \lb}  \label{OIGJ:LinkedList}
\STATE \code{~~Entry<\underline{This,I},E> header;} \label{OIGJ:header}
\STATE \code{~~\underline{<I extends Raw>?} LinkedList() \lb} \label{OIGJ:Raw:ctor1}
\STATE \code{~~~~this.header = new Entry<\underline{This,I},E>();} \label{OIGJ:Raw:I1}
\STATE \code{~~~~header.next = header.prev = header;} \label{OIGJ:assignment:ctor1} %
\STATE \code{~~\rb}
\STATE \code{~~\underline{<I extends Raw>?} LinkedList(} \label{OIGJ:Raw:ctor2}
\STATE \code{~~~~~~~~~~~~~~~~~Collection<\underline{?,ReadOnly},E> c) \lb}
\STATE \code{~~~~this();~~this.addAll(c);} \label{OIGJ:call-ctor1}
\STATE \code{~~\rb}
\STATE \code{~~\underline{<I extends Raw>?} void addAll(} \label{OIGJ:addAll:definition}
\STATE \code{~~~~~~~~~~~~~~~~~Collection<\underline{?,ReadOnly},E> c) \lb}
\STATE \code{~~~~Entry<\underline{This,I},E> succ = this.header,} \label{OIGJ:Raw:I2} %
\STATE \code{~~~~~~~~~~~~~~~~~~~~pred = succ.prev;} %
\STATE \code{~~~~for (E e : c) \lb}
\STATE \code{~~~~~~Entry<\underline{This,I},E> en=new Entry<\underline{This,I},E>();}
\STATE \code{~~~~~~en.element=e; en.next=succ;~en.prev=pred;}
\STATE \code{~~~~~~pred.next = en;~~pred = en;~~\rb} \label{OIGJ:assignment:addAll} %
\STATE \code{~~~~succ.prev = pred;} \label{OIGJ:assignment:addAll:prev}
\STATE \code{~~\rb} \label{OIGJ:Raw:end}
\STATE \code{~~int size() \lb\ldots\rb} \label{OIGJ:size}
\STATE \code{~~}\myCOMMENT{\code{iterator} is a generic method; this is not a cJ guard:}
\STATE \code{~~\underline{<ItrI extends ReadOnly>} Iterator<\underline{O,ItrI,I},E>} \label{OIGJ:iterator}
\STATE \code{~~~~~~~~~~~~~~~~~iterator() \lb}
\STATE \code{~~~~return this.new ListItr<\underline{ItrI}>();} \label{ListItr:create}
\STATE \code{~~\rb}
\STATE \code{~~void remove(Entry<\underline{This,Mutable},E> e) \lb}
\STATE \code{~~~~e.prev.next = e.next;} \label{ListItr:prev}
\STATE \code{~~~~e.next.prev = e.prev;} \label{ListItr:prev2}
\STATE \code{~~\rb}
\STATE \code{~~class ListItr<\underline{ItrI}> implements} \label{ListItr:start}
\STATE \code{~~~~~~~~Iterator<\underline{O,ItrI,I},E> \lb} \label{ListItr:Iterator}
\STATE \code{~~~~Entry<\underline{This,I},E> current;} \label{OIGJ:assignable} %
\STATE \code{~~~~\underline{<ItrI extends Raw>?} ListItr() \lb} \label{ListItr:ctor}
\STATE \code{~~~~~~this.current = LinkedList.this.header;} \label{ListItr:ctor-assignment}
\STATE \code{~~~~\rb}
\STATE \code{~~~~\underline{<ItrI extends Mutable>?} E next() \lb} \label{ListItr:next}
\STATE \code{~~~~~~this.current = this.current.next;} \label{ListItr:next-assignment}
\STATE \code{~~~~~~return this.current.element;}
\STATE \code{~~~~\rb}
\STATE \code{~~~~\underline{<I extends Mutable>?} void remove() \lb} \label{ListItr:remove}
\STATE \code{~~~~~~LinkedList.this.remove(this.current);} \label{ListItr:remove-call}
\STATE \code{~~~~\rb}
\STATE \code{\rb~\rb}\label{ListItr:end}
%
\STATE \code{interface Iterator\hgn{\underline{O,ItrI,CollectionI},E} \lb }  \label{I:Iterator}
\STATE \code{\quad boolean hasNext(); } \label{I:hasNext}
\STATE \code{\quad \underline{<ItrI extends Mutable>?} E next(); }  \label{I:next}
\STATE \code{\quad \underline{<CollectionI extends Mutable>?} void remove(); } \label{I:remove}
\STATE \code{\rb\ } \label{I:Iterator:end}
\end{algorithmic}
\caption{\code{LinkedList<\nounderline{O,I},E>} in OIGJ\@.}
%
%
\label{Figure:OIGJ-LinkedList}
\end{figure}

%



\paragraph{Immutable object creation}
A constructor that is making an immutable object must be able to set the fields of the object.
It is not acceptable to mark such constructors as \Mutable, %
    which would permit arbitrary side effects, possibly including making mutable aliases to \code{this}.
OIGJ uses a fourth kind of immutability,~\Raw,
    to permit constructors to perform limited side effects without
    permitting modification of immutable objects.
%
\Raw represents a partially-initialized \emph{raw}
    object that can still be arbitrarily mutated, but after
    it is cooked (fully initialized), then the object might become immutable.
The constructors on lines~\ref{OIGJ:Raw:ctor1} and~\ref{OIGJ:Raw:ctor2}
    are guarded with \Raw, and therefore
    can create both mutable and immutable lists.
%

Objects must not be captured in their raw state to prevent further mutation after the object is cooked.
If a programmer could declare a field, such as \code{Date\hgn{O,\Raw{}}},
    then a raw date could be stored there, and later it could be used to mutate a cooked immutable date.
Therefore, a programmer can write the \Raw{} type only after the \code{extends} keyword, but
    \emph{not} in any other way.
%
%
As a consequence, in a \Raw{} constructor, \this can only escape as \ReadOnly.

Recall that an object becomes \emph{cooked} either
    when its constructor finishes
    or when its owner is \emph{cooked}.
The entries of the list (line~\ref{OIGJ:header}) are \this-owned.
Indeed, the entries are mutated after their constructor finished, but before the list is cooked,
    on lines~\ref{OIGJ:assignment:ctor1}, \ref{OIGJ:assignment:addAll}, and \ref{OIGJ:assignment:addAll:prev}.
This shows the power of combining immutability and ownership:
    we are able to create immutable lists \emph{only} by using the fact that the list owns its entries.
If those entries were \emph{not} owned by the list, then this mutation of entries might be visible
    to the outside world, thus breaking the guarantee that an immutable object never changes.
By enforcing ownership, OIGJ ensures that such illegal mutations cannot occur.


%
%
%
%
%
%
%
%


OIGJ requires that all access and assignment to a \this-owned field
    must be done via \this. %
For example, see \code{header}, on lines~\ref{OIGJ:Raw:I1},~\ref{OIGJ:assignment:ctor1},~\ref{OIGJ:Raw:I2},
    and~\ref{ListItr:ctor-assignment}.
In contrast, fields \code{next} and \code{prev} (which are not \this-owned)
    do not have such a restriction,
    as can be seen on lines~\ref{ListItr:prev}--\ref{ListItr:prev2}.




\paragraph{Iterator implementation and inner classes}
An \emph{iterator} has an underlying \emph{collection}, and the immutability
    of these two objects might be different.
For example, you can have
\begin{itemize}\itemsep 0pt \parskip 0pt
\item
    a mutable iterator over a mutable collection
    (the iterator supports both \code{remove()} and \code{next()}),
\item
    a mutable iterator over a readonly/immutable collection
    (the iterator supports \code{next()} but not \code{remove()}), or
\item
    a readonly iterator over a mutable collection
    (the iterator supports \code{remove()} but not \code{next()},
    which can be useful if you want to pass an iterator to a method that may not advance the iterator but may remove the current element).
\end{itemize}

Consider the \code{Iterator<O,ItrI,CollectionI,E>} interface
    defined on lines~\ref{I:Iterator}--\ref{I:Iterator:end},
    and used on lines~\ref{OIGJ:iterator} and~\ref{ListItr:Iterator}.
\code{ItrI} is the iterator's immutability, whereas
    \code{CollectionI} is intended to be the underlying collection's immutability
    (see on line~\ref{ListItr:Iterator} how the collection's immutability~\hI is used in the place of \code{CollectionI}).
Line~\ref{I:next} requires a mutable \code{ItrI} to call \code{next()},
    and line~\ref{I:remove} requires a mutable \code{CollectionI} to call \code{remove()}.

Inner class \code{ListItr} (lines~\ref{ListItr:start}--\ref{ListItr:end})
    is the implementation of \code{Iterator} for list.
Its full name is \code{LinkedList<O,I,E>.List\-Itr<ItrI>},
    and on line~\ref{ListItr:start} it extends \code{Iterator<O,ItrI,I,E>}.
%
It reuses the owner parameter \code{\underline{O}} from \code{LinkedList},
    but declares a new immutability parameter \code{\underline{ItrI}}.
An inner class, such as \code{ListItr<ItrI>}, only declares an immutability parameter
    because it inherits the owner parameter from its outer class.
\code{ListItr} and \code{LinkedList} have the same owner~\hO,
    but different immutability parameters (\code{ItrI} for \code{ListItr}, and \code{I} for \code{LinkedList}).
\code{ListItr} must inherit \code{LinkedList}'s owner because it directly accesses the (\this-owned)
    representation of \code{LinkedList} (line~\ref{ListItr:ctor-assignment}),
    which would be illegal if their owner was different.
For example, consider the types of \code{this} and \code{LinkedList.this}
    on line~\ref{ListItr:ctor-assignment}:
\begin{algorithmic}
\STATE\code{Iterator<\underline{O,ItrI},\ldots> thisIterator = this;} \\
\STATE\code{LinkedList<\underline{O,I},\ldots> thisList = LinkedList.this;} \\
\end{algorithmic}
Because line~\ref{ListItr:ctor} sets the bound of~\code{ItrI} to be \Raw,
    \this can be mutated.  By contrast, the bound of \hI is \ReadOnly, so
\code{LinkedList.this} cannot.


%
%
%

%
An inner class must have a distinct immutability parameter,
    but it must reuse the owner parameter of its outer class.
%
%
%
%
%
%
%
%
%
We could have several \This types, e.g., \code{LinkedList.This} vs.\ \code{ListItr.This},
    but this would complicate the typing rules.
%

%
%

Finally, consider the creation of a new \emph{inner} object on line~\ref{ListItr:create}
    using \code{\underline{this}.new ListItr<ItrI>()}.
This expression is type-checked both as a method call (whose receiver is \this)
    and as a constructor call.
Observe that the bound of \code{ItrI} is \ReadOnly (line~\ref{OIGJ:iterator})
    and the guard on the constructor is \Raw (line~\ref{ListItr:ctor}),
    which is legal because a \Raw constructor can create both mutable and immutable objects.









\Subsection[typing-rules]{OIGJ typing rules}

\begin{figure}[!t]
\begin{smaller}
\def\codesmaller{\smaller}
\begin{description}
  \item[Ownership nesting]
    The first owner parameter of type~\hT must be inside
        any other owner parameter in~\hT.

  \item[Field access]
    Field access~\code{o.f} is legal
        iff~\underline{$\Ofn{\code{f}}=\This \Rightarrow \code{o}={\this}$}.

  \item[Field assignment]
    Field assignment~\code{o.f=\ldots} is legal iff
        (i)~$\Ifn{\code{o}} \st \Raw$, and
        (ii)~$\big(\Ifn{\code{o}} = \Raw \Rightarrow (\code{o}=\this\text{~or~}\Ofn{\code{o}} = \This)\big)$, and
        (iii)~field access~\code{o.f} is legal.

  \item[Method invocation]
    Consider method~\code{T$_0$ m(T$_1$,\ldots,T$_n$)}.
    The invocation~\code{o.m(\ldots)} is legal
        iff
        (i)~\underline{$\Ofn{\code{T}_i}=\This \Rightarrow \code{o}={\this}$} for~$i=0,\ldots,n$, and
        (ii)~$\Ifn{\code{m}} = \Raw$ implies field assignment part (ii).

    %
    %

  \item[cJ's method guard]
    (i)~An invocation~\code{o.m(\ldots)} is legal if the type of~\code{o} satisfies the guard of~\code{m}.
    (ii)~When typing method~\hm, the bound of type variables that appear in the guard
        changes to their bound in the guard.
    (iii)~The guard of an overriding method is
        equivalent or weaker than that of the overridden method.

  \item[Inner classes]
    An inner class reuses the owner parameter of the outer class.
    However, it has a distinct immutability parameter.

  \item[Invariant]
    The programmer marks each type parameter as invariant or covariant.
%
%
%
%
%
    An immutability parameter is always covariant,
     whereas an owner parameter is always invariant.

    A type parameter must be invariant if it is used in
        a superclass that contains \Mutable,
        a field that contains \Mutable but is not \this-owned,
        or in the position of another invariant type parameter.


  \item[Same-class subtype relation]
    Let $\hC\hgn{\hX_1,\ldots,\hX_n}$ be a class.
    Type $\hS=\hC\hgn{\hS_1,\ldots,\hS_n}$ is
        \emph{a subtype of} $\hT=\hC\hgn{\hT_1,\ldots,\hT_n}$,
        written as $\hS\st\hT$,
        iff
        ($\hS=\hT$) or
        \Big((all immutability parameters $\hT_j$ are either \ReadOnly{} or \Immut{}),
        and for~$i=1,\ldots,n$, \big($\hS_i=\hT_i$ or ($\hS_i \st \hT_i$ and $\hX_i$ is covariant in \hC)\big)\Big).
%

  \item[Erased signature]
    If method~\code{m}$'$ overrides a readonly/immutable method~\code{m}, %
        then the erased signatures of~\code{m}$'$ and~\code{m}, excluding invariant
        type parameters, must be identical.
    (The \emph{erased signature} of a method is obtained by replacing type parameters
        with their bounds.)

  \item[Object creation]
    A constructor cannot have any \this-owned arguments.
    Furthermore, \code{new SomeClass\hgn{X,\ldots}(\ldots)} is legal iff
        the constructor's guard \code{<I extends Y>?}
        satisfies:
        $\code{Y}=\Mutable$ and $\code{X}=\Mutable$, or $\code{Y}=\Raw$.

  \item[Generic Wildcards]
    OIGJ prohibits using a generic wildcard (\code{?})
        in the position of the immutability parameter.
    For the owner parameter,
        OIGJ prohibits using a wildcard in a field or in a method return type,
        but permits it
        for stack variables and method parameters.

  \item[\Raw parameter]
    \code{Raw} can only be used after the {\code{extends}} keyword.
    It cannot be used in the position of
        a generic parameter.

  \item[Fresh owners]
    A \emph{fresh owner} is a method owner parameter
        that is not used in the method signature.
    It is a descendant in the ownership tree of all other owners in scope.

  \item[Static context]
    \This{} cannot be used in a static context (static methods or \rlap{fields).}
\end{description}
\end{smaller}
\def\codesmaller{\small}
\caption{All the OIGJ typing rules (beyond those of Java), in English.  Also see \Ref{Section}{formal} for
  a formalization. Underlined sentences show similarities among the rules.
  }
\label{Figure:oigj-typing-rules}
\end{figure}

%


\Ref{Figure}{oigj-typing-rules} contains all the OIGJ typing rules.
We now discuss each rule.
\Ref{Section}{formal} presents a formal type system based on a simplified version of these rules.
Some of the rules are identical to those found
    in OGJ~\cite{PotaninNCB2006} and IGJ~\cite{ZibinPAAKE2007}
    (see \Ref{Section}{related-work} for a comparison with OIGJ).

\paragraph{Ownership nesting}
Consider the following example:
\begin{algorithmic}
\STATE \code{List<\underline{This},I,Date<\underline{World},I>> l1;} \myCOMMENT{Legal nesting}
\STATE \code{List<\underline{World},I,Date<\underline{This},I>> l2;} \myCOMMENT{Illegal!}
\end{algorithmic}
Definition of \code{l2} has illegal ownership nesting
    because owned dates might leak, e.g., we can store \code{l2} in this variable:\\
\code{public static Object<World,ReadOnly> publicAliasToL2;}

On the one hand, types in OIGJ may have multiple owner parameters, e.g., the type of \code{l1} has two owner parameters (\This and \World).
On the other hand, an object may only have a single owner at run time.
For example, the type of \code{l1} will correspond at run time to a list that is owned by \this while its elements are owned by \World,
    and observe that \this is always inside \World.

Recall that an owner $o_1$ is \emph{inside} $o_2$ iff $o_1$ is a descendant in the ownership tree of $o_2$, i.e., $o_1 \Oprec o_2$.
We extend this definition from owners to owner parameters as follows:
    given two owner parameters~$\code{O}_1$ and~$\code{O}_2$ in the same type,
    then~$\code{O}_1$ is \emph{inside}~$\code{O}_2$ iff
    in any possible execution, these owner parameters correspond to some owners $o_1$ and $o_2$ (respectively) where $o_1 \Oprec o_2$.
For example, \This is inside \code{O}, and any owner parameter is inside \World.

OIGJ requires that owner parameters are properly nested, i.e.,
    that the first owner parameter of type~\hT is inside
    any other owner parameter in~\hT.
To enforce this rule, OIGJ maintains ordering constraints among owner parameters
    in the same way as described in OGJ~\cite{PotaninNCB2006}.



\paragraph{Field access}
This rule enforces ownership:
    \this-owned fields can be assigned only via \this.
In \Ref{Figure}{OIGJ-LinkedList}, note that all accesses and assignments to \code{header} are done via \this.
    %

\paragraph{Field assignment}
Assigning to a field should respect both immutability and ownership constraints.
Part (i) of the rule enforces immutability constraints:
a field can be assigned only by a \Mutable or \Raw reference.
Part (ii) ensures \Raw is transitive only for \this or \this-owned objects.
Part (iii) enforces ownership constraints as in field access.

For example, consider
    the assignments
    on lines~\ref{OIGJ:Raw:I1} %
    and~\ref{OIGJ:assignment:ctor1} %
    of \Ref{Figure}{OIGJ-LinkedList}.
Note that the bound of \hI is \Raw{}, thus the assignments satisfy part (i).
Part (ii) holds, i.e., \Raw is transitive in the first assignment because the target object is \this
    and in the second assignment because it is \this-owned (the type of \code{this.header} is \code{Entry<\underline{\This},I,E>}).
Finally, part (iii) holds in the first assignment because \code{header} was assigned via \this,
    and in the second assignment because field \code{next} (\code{Entry<\underline{O},I>}) is not \this-owned.



\paragraph{Method invocation}
Method invocation is handled in the same way as field access/assignment:
    parts (i) and~(ii) are similar to field access and field assignment part (ii).
For example, consider the following method:~~~\code{R m(A a) \lb~\ldots~\rb}\\
Then, the method call \code{o.m(e)} is handled as if there is an assignment
    to a field of type \code{A},
    and the return value is typed as if there was an access to a field of type \code{R}\@.
Note that regarding the transitivity of \Raw, we check both
    the immutability of the receiver object (\Ifn{\code{o}})
    and that of the method, i.e., its guard (\Ifn{\code{m}}).
If both are \Raw, then we require that \code{o} is either \this or \this-owned.


\paragraph{Inner classes}
An \emph{inner class} is a non-static nested class, e.g.,
    iterators in \code{java.util} are implemented using inner classes.
An inner class reuses the owner parameter of the outer class,
    i.e.,  the inner object is seen as an extension of the outer object.
However, it has a distinct immutability parameter.
Therefore, both \this and \code{OuterClass.this} are treated identically
    by the typing rules that involve ownership.
%
%

Nested classes that are \emph{static} can be treated the same as normal classes.

%
%
%
%
%
%



\paragraph{Invariant}
A user can annotate a type parameter~\hX in class~\hC
    with \InVariantAnnot
    to prevent covariant changes,
    in which case we say that~\hX is invariant.
Otherwise we say that~\hX is covariant.
An \iparam must be covariant,
    or else a mutable reference could not be a receiver when calling a readonly method.
An owner parameter must be invariant, because the owner of an object cannot change.

A type parameter must be invariant
    if it is used in a field/superclass that contains \Mutable, or if the erased signature differs.
For example, if a class has a field of type \code{Foo<O,Mutable,X>},
    then \code{X} must be invariant (the owner parameter \code{O} is always invariant).



\paragraph{Subtype relation}
Java is \emph{invariant} in generic arguments, i.e., it prohibits \emph{covariant} (or contravariant)
    changes.
\code{Vector<\discretionary{}{}{}Integer>} is not a subtype of \code{Vector<Object>}.
If it were, then mutating a \code{Vector<Integer>} by inserting,
    e.g., a \code{String}, breaks type-safety.

OIGJ permits covariant changes for non-mutable references
    because the object cannot be mutated in a way that is not type-safe.
OIGJ's subtyping rules includes Java's subtyping rules,
    therefore OIGJ's subtype relation is a superset of Java's subtype relation.
If mutation is disallowed, OIGJ's subtyping rule allows covariant changes
    in other type parameters, within the \emph{same class}.
For example,
        \code{List\hgn{O,{\ReadOnly},\underline{Integer}}} is a subtype of
        \code{List\hgn{O,{\ReadOnly},\discretionary{}{}{}\underline{Number}}}. %
        %
            %
        %
Note that covariance is allowed iff \emph{all} immutability parameters of the supertype are
    \ReadOnly{} or \Immut{}, e.g.,
    \code{Iterator\hgn{O,\ReadOnly,\Mutable,{Integer}}} is \emph{not} a subtype of
    \code{Iterator\hgn{O,\discretionary{}{}{}{\ReadOnly},\underline{\Mutable},{Number}}}, but it is a subtype of
    \code{Iterator\hgn{O,{\ReadOnly},\underline{\ReadOnly},{Number}}}.


\paragraph{Erased signature}
When the erased signature of an overriding method differs from the overridden method,
    the normal \code{javac} compiler inserts a \emph{bridge method} to cast the
    arguments to the correct type~\cite{BrachaOSW98}.
Such bridge methods work correctly only under the assumptions that subtyping is invariant.
For example, consider an integer comparator~\code{intComp}
    that implements \code{Comparable<Integer>}.
If \code{Comparable<Integer>} were a subtype of
    \code{Comparable<Object>}, then we could pass a \code{String} to
    \code{intComp}'s implementation of \code{compareTo(Integer)}:\\
\code{((Comparable<Object>)intComp).compareTo("a")}

OIGJ requires that the \emph{erased signature}
    of an overriding method remains the same (excluding invariant
    parameters)
    if the overridden method is either readonly or immutable.
For example, the erased signature of \code{compareTo} in~\code{intComp}
    differs from the one in the interface \code{Comparable<O,I,X>}.
Therefore, this rule requires that the type parameter~\hX must be invariant:

\begin{algorithmic}
\STATE \code{interface Comparable\hgn{O,\IP, \InVariantAnnot X} \lb\ }
\STATE \code{~~int compareTo(X o); \rb}
%
%
%
%
\end{algorithmic}



\paragraph{Object creation}
A constructor should not have any \this-owned parameters, because
    \this-owned objects can only be created inside \this.
%
%
%
%
%

Recall that the immutability of a constructor (or any method in general) is defined to be the bound
    of the immutability parameter in that constructor,
    e.g., a mutable constructor has the guard \code{<I extends Mutable>?}.
Recall that cJ prohibits calling a \Raw constructor to create an \Immut object
    because the guard is not satisfied:
    \Immut{} is not a subtype of \Raw{}.
OIGJ changed cJ and treats constructor calls using this object creation rule:
a \Raw{} constructor %
    can create any object (mutable and immutable).
A \Mutable constructor can only create \Mutable objects.
A constructor cannot be \Immut or \ReadOnly, so that it is able to assign to the fields of \this.

%
%
%
%
%
%
%
%
%




\paragraph{Generic wildcards}

OIGJ uses Java's existing generic wildcard syntax (\code{?}) to
    express existential owners~\cite{WrigstadC2007,CameronD2009,OstlundWC2008}.
One can use existential
    owners
    when the exact owner of an object is unknown.
A motivation for existential owners is the
    downcast performed in the \code{equals} method~\cite{WrigstadC2007}.

Consider the following two casts in normal Java:
\begin{algorithmic}
\STATE \code{boolean equals(Object o)}
\STATE \code{\lb~~List<?> l = (List<?>)o;}~~\myCOMMENT{OK}
\STATE \code{~~~List<Object> l = (List<Object>)o;~\rb}~~\myCOMMENT{Warning!}
%
\end{algorithmic}
The second cast is a warning
    since erasure makes it impossible to
    %
    check at run time that the generic parameter is \code{Object}.

OIGJ prohibits wildcards on the owner parameter of \emph{fields},
    e.g., \code{Date<?,ReadOnly> field},
    because one can declare a static field of that type and store a \this-owned date,
    thus breaking owner-as-dominator.
Wildcards on a method return type are also prohibited because they can be used to leak
    \this-owned fields. %
However, wildcards on \emph{stack variables} (method parameters or local variables)
    are allowed.


%
%
Note that the immutability parameter is covariant, and therefore there is no need to use a wildcard for immutability.
For example, consider the \code{DateList} class, which is parameterized by its owner parameter (\code{O})
    and the dates' owner parameter (\code{DO}):

\begin{algorithmic}
\STATE \code{class DateList<O,I,DO extends World> \lb}
\STATE \code{~boolean equals(Object<?,ReadOnly> o)}
\STATE \code{~\lb~DateList<?,ReadOnly,?> l =}
\STATE \code{~~~~\,}\myCOMMENT{No need to check ownership or immutability at run time.}
\STATE \code{~~~~(DateList<?,ReadOnly,?>) o;}
\STATE \code{~~~return listEquals(l);~\rb}
%
\STATE \code{~<O2 extends World,DO2 extends World> boolean}
\STATE \code{~~~~listEquals(DateList<O2,ReadOnly,DO2> l) \lb\ldots\rb}
\STATE \code{\rb}
\end{algorithmic}

\noindent
Method \code{listEquals} shows that it is possible to name
    the existential owner---the unknown list's owner parameter is \code{O2} and the unknown dates'
    owner parameter is \code{DO2}.
Phrased differently, the two wildcards in \code{DateList<\underline{?},ReadOnly,\underline{?}>} are now named
    \code{DateList<\underline{O2},ReadOnly,\underline{DO2}>}.
Although wildcards can sometimes be replaced by generic methods,
    wildcards are necessary in downcasts (as shown in method \code{equals}).


Recall that
Java's generics can be bypassed by using reflection or raw types such as \code{List}.
Similarly, one can bypass OIGJ when using these features.


\paragraph{\Raw{} parameter}
\code{Raw} can only be used
    after the \underline{\code{extends}} keyword.
For example, it is prohibited to write \code{Date<O,\underline{\Raw{}}>}.
If this was possible, then such a date could leak from a \Raw constructor
    that is building an immutable object resulting in
    %
    an alias that could mutate such immutable object.


\paragraph{Fresh owner}
A \emph{fresh owner} is a method owner parameter
    that is not used in the method signature.
In OIGJ, a fresh owner expresses \emph{temporary ownership} within the method.
%
This allows a method to create stack-local
    objects with access to any object visible at the point of creation,
    but with a guarantee
    that stack-locals will not leak.
Hence, stack-local objects can be garbage-collected when the method {re\-turns}.
For example, consider a method that deserializes a \code{{By\-te\-Stream}} by creating a temporary
    \code{ObjectStream} wrapper:
\begin{algorithmic}
\STATE \code{<O,\underline{TmpO}> void deserialize(ByteStream<O> bs) \lb}
\STATE \code{~~ObjectStream<\underline{TmpO},ByteStream<O>> os = \ldots~\rb}
\end{algorithmic}
Note that \code{TmpO} is a fresh owner, whereas \code{O} is not.
%
Because \code{TmpO} is strictly inside other owner parameters such as \code{O},
    there cannot be any aliases from \code{bs} to \code{os}.
In fact, \code{os} can only be referenced from other stack-local objects,
    and therefore, when the method returns, \code{os} can be garbage-collected.

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%


Technically,
    \emph{a fresh owner is strictly inside all other non-fresh owners in scope},
        to make sure it cannot exist after the method returns.
(Multiple fresh owners are incomparable with each other.)
Because a fresh owner is inside several other owners that might
        be incomparable in the ownership tree, the ownership structure is a
        DAG rather than a tree.

To type-check temporary ownership and DAG ownership structures,
    OIGJ adopts Wrigstad's \emph{scoped confinement}~\cite{Wrigstad2006}
    ownership model,
    in which the fresh owners are owned by the current \emph{stack-entry}.
Briefly stated, each method invocation pushes a new stack-entry
    (the first stack-entry corresponds to the static \code{main} method),
    which is the root of a new ownership tree.
Objects in this new tree may point to objects in previous trees, but not
    vice versa.
%
%
%
%


\paragraph{Static context}
\This represents that an object is owned by \this,
    and so OIGJ prohibits using it in a static context,
    such as static fields or methods.
Static fields can use the {ow\-ner} parameter \World, and static methods can also use
    {gene\-ric} method parameters extending \World.
For example, method: %

\begin{algorithmic}
\STATE \code{static <LO extends World,E> void sort(}\\
\STATE \code{~~~~~~~~~~~~~~~~~~~~List<LO,Mutable,E> l) \lb~\ldots~\rb}\\
\end{algorithmic}
    is parameterized by the list's owner \code{LO}.

%
%
%
%
%




\Subsection[Factory]{Factory method design pattern}

The \emph{factory method pattern}~\cite{designpatterns}
    is a creational design pattern
    for creating objects
    without specifying the exact class of the object that will be created.
The solution is to define an interface with a method for creating an object.
Implementers can override the method to create objects of a derived type.

The challenge of the factory method pattern with respect to
    \emph{ownership}~\cite{Nageli2006}
    is that the point of \emph{creation} and \emph{usage} are in different classes,
    and the created object must be owned by its user.
Previous work makes a newly-created object be owned by its creator, and
    then changes the ownership after the fact via
    sophisticated ownership transfer mechanisms~\cite{MullerR2007}
    using \code{capture} and \code{release}.


\begin{figure}[t]
\begin{algorithmic}[1]
\STATE \code{\mbox{class SafeSyncList<\nounderline{O,I},E> implements List<\nounderline{O,I},E> \lb}} \label{SafeSyncList:start}
\vspace{-2.7ex}
\STATE \code{~~List<\nounderline{This,I},E> l;} \label{SafeSyncList:l}
\STATE \code{~~\nounderline{<I extends Raw>?} SafeSyncList(} \label{SafeSyncList:factory-start}
\STATE \code{~~~~~~~~~~~~~~~~~~~~Factory<\nounderline{?,ReadOnly},E> f)}
\STATE \code{~~\lb~List<\nounderline{This,I},E> b = f.create();} \label{SafeSyncList:b}
\STATE \code{~~~~l = Collections.synchronizedList(b);~\rb} \label{SafeSyncList:usage} \label{SafeSyncList:factory-end}
%
\STATE \code{~~\ldots} \myCOMMENT{delegate methods to \code{l}}
\STATE \code{\rb} \label{SafeSyncList:end}
\STATE \code{class Collections<\nounderline{O,I}> \lb}
\STATE \code{~~}\myCOMMENT{Sun's~original~\mbox{implementation},~\mbox{augmented}~only~by~\code{O2}~and~\code{I2}}
\STATE \code{~~static~<\nounderline{O2,I2},E>~List<\nounderline{O2,I2},E> }
\STATE \code{~~~synchronizedList(List<\nounderline{O2,I2},E> list)~\lb~\ldots~\rb  }
%
\STATE \code{\rb}
\STATE \code{interface Factory<\nounderline{O,I},E> } \label{Factory:start}
\STATE \code{\lb~~<\nounderline{O2,I2}> List<\nounderline{O2,I2},E> create();~~\rb} \label{Factory:generic-method} \label{Factory:end}
%
\STATE \code{class LinkedListFactory<\nounderline{O,I},E> implements}
\STATE \code{~~~~~~~~~~~~~~~~Factory<\nounderline{O,I},E> \lb}
\STATE \code{~~<\nounderline{O2,I2}>~List<\nounderline{O2,I2},E> create() \lb} \label{SafeSyncList:generic-method}
\STATE \code{~~~~return new LinkedList<\nounderline{O2,I2},E>();} \label{SafeSyncList:capture}
\STATE \code{\rb~\rb}
%
\end{algorithmic}
\caption{Factory method design pattern in OIGJ\@.\
OIGJ guarantees that the backing list \code{b} (line~\ref{SafeSyncList:b}) is never accessed directly,
    e.g., it cannot be captured on line~\ref{SafeSyncList:capture}.}
\label{Figure:OIGJ-Factory-method}
\end{figure}


In OIGJ's approach, an object has its final owner from its moment of creation.
When requesting creation of a new object,
the client of the factory also specifies the owner.
The type-checker ensures that
the created object cannot be \emph{captured} (stored in a location that
would require a different owner) in the process.
Specifically, a \emph{generic factory method} can
    abstract over the owner (and immutability) parameter of the constructed
    object.
The underlying generics mechanism finds the correct generic method arguments.

We will show how to use the factory method pattern
    in the context of \emph{synchronized lists}.
%
%
%
%
%
%
%
%
%
%
%
%
Consider this client code:

\begin{algorithmic}
\STATE \code{b = new LinkedList<T>();}
\STATE \code{l = Collections.synchronizedList(b);}
\end{algorithmic}
The documentation of \code{Collections.synchronizedList} states:
``\emph{In order to guarantee serial access, it is \emph{critical} that all access to the backing list is accomplished through the returned list.}"
That means that there might be concurrency problems
    if one %
    accidentally uses the backing list~\code{b} instead of~\code{l}. %

%
%
%
%
%
%

So, you want to own a list \code{l}, which is backed by another list \code{b}.
The challenge is that \code{b} should be owned by \code{l} (and not by you),
    in order to guarantee that you do not accidentally access \code{b} directly  and comprise thread-safety.

%
%
%
%
%

\Ref{Figure}{OIGJ-Factory-method} shows how
    owner-as-dominator can ensure that the backing list~\code{b} has no
    outside aliases.
This solution avoids refactoring of existing Java code
    by delegating calls to the synchronized list~\hl.
Specifically, class \code{SafeSyncList} (lines~\ref{SafeSyncList:start}--\ref{SafeSyncList:end})
    owns both the list \code{l} (line~\ref{SafeSyncList:l})
    and the backing list \code{b} (line~\ref{SafeSyncList:b}).
A factory method is used
    on lines~\ref{SafeSyncList:factory-start}--\ref{SafeSyncList:factory-end}.



The \code{Factory} interface is defined on lines~\ref{Factory:start}--\ref{Factory:end}.
The owner and immutability of the \code{Factory} is irrelevant
    because it only has a readonly method.
However, the newly created list has a generic owner and immutability,
    which are statically unknown at the creation point (line~\ref{Factory:generic-method}).
The generics mechanism fills in the correct generic arguments
    from the usage point (line~\ref{SafeSyncList:usage})
    to the actual creation point (line~\ref{SafeSyncList:capture}).
Note that the factory implementation cannot capture an alias to the
    newly created list on line~\ref{SafeSyncList:capture},
    because its owner parameter~\code{O2} is a generic method parameter
    that cannot be used in fields.

To conclude, one can use \code{SafeSyncList} instead of using Sun's unsafe \code{synchronizedList},
     and be certain no one else can access the backing list.
All this was achieved using \emph{generic factory methods} on
    lines~\ref{Factory:generic-method} and~\ref{SafeSyncList:generic-method}.


\Subsection[Visitor]{Visitor pattern}

The \emph{visitor design pattern}~\cite{designpatterns} is a way of
    separating an algorithm from
    a node hierarchy upon which it operates.
Instead of distributing the node processing code among all the node
    implementations,
    the algorithm is written in a single \emph{visitor} class
    that has a visit method for every node in the hierarchy.
This is desirable when the algorithm changes frequently or when
    new algorithms are frequently created.
The standard implementation (that does not use reflection)
    defines a tiny \code{accept} method that is overridden in all the nodes,
    that calls the appropriate visit method for that node.


\begin{figure}[t]
\begin{algorithmic}[1]
\STATE \code{interface Visitor<O,I,\underline{NodeO,NodeI}> \lb} \label{Visitor:start}
%
\STATE \code{~<I extends Mutable>? void} \label{Visitor:visit}
\STATE \code{~~~visit(Node<\underline{NodeO,NodeI}> n);}
\STATE \code{\rb} \label{Visitor:end}
\STATE \code{class Node<\underline{O,I}> \lb}
\STATE \code{~void accept(Visitor<?,Mutable,\underline{O,I}> v)} \label{Visitor:accept}
\STATE \code{~\lb~~v.visit(this)~~\rb}
%
\STATE \code{\rb}
\STATE \myCOMMENT{Visiting a readonly node hierarchy.}
\STATE \code{Node<\underline{This,ReadOnly}> readonlyNode = \ldots;} \label{Visitor:match1:ReadOnly}
\STATE \code{readonlyNode.accept( new }
\STATE \code{~Visitor<World,Mutable,\underline{This,ReadOnly}>() \lb} \label{Visitor:match2:ReadOnly}
\STATE \code{~~<I extends Mutable>? void}
\STATE \code{~~~~visit(Node<\underline{This,ReadOnly}> n)}\label{Visitor:visit:ReadOnly}
\STATE \code{~~~~\lb~\ldots} \myCOMMENT{Can mutate the visitor, but not the nodes.} \code{~\rb}
%
\STATE \code{~\rb);}
\STATE \myCOMMENT{Visiting a mutable node hierarchy.}
\STATE \code{Node<\underline{This,Mutable}> mutableNode = \ldots;} \label{Visitor:match1:Mutable}
\STATE \code{mutableNode.accept( new }
\STATE \code{~Visitor<World,Mutable,\underline{This,Mutable}>() \lb} \label{Visitor:match2:Mutable}
\STATE \code{~~<I extends Mutable>? void}
\STATE \code{~~~~visit(Node<\underline{This,Mutable}> n)}\label{Visitor:visit:Mutable}
\STATE \code{~~~~\lb~\ldots} \myCOMMENT{Can mutate the visitor and the nodes.} \code{~\rb} \label{Visitor:visit:Mutable:capture}
%
\STATE \code{~\rb);}
\end{algorithmic}
\caption{Visitor pattern in OIGJ\@. The \code{Node}'s ownership and immutability are underlined.
    We omit the \code{extends} clause
        for generic parameters, e.g., we assume that \code{NodeO extends World}.
    A single visitor interface can be used both for \Mutable and \ReadOnly nodes.
    }
\label{Figure:OIGJ-Visitor-pattern}
\end{figure}


N{\"a}geli~\cite{Nageli2006} discusses ownership
    in design patterns, and shows that previous \emph{ownership} work was not flexible enough
    to express the visitor pattern.
A visitor is always mutable because it may accumulate information during the traversal of the nodes hierarchy.
However, some visitors only need readonly access to the nodes,
    and some need to modify the nodes.
In the former case, the owner of the visitor and nodes may be different,
    and in the latter case, it must be the same owner.
The challenge is to use the same \code{visit} and \code{accept} methods,
    and to avoid duplicating the traversal code.

OIGJ can express the visitor pattern by relying on
owner-polymorphic methods:
    the owner of an object~\code{o}, can pass it to
    an  \emph{owner-polymorphic method}, which cannot
    capture~\code{o}.

%
%
%
%
%
%
%
%
%
%

\Ref{Figure}{OIGJ-Visitor-pattern} shows the visitor pattern in OIGJ\@.
As mentioned before, the \emph{owner} of the visitor and nodes may be different,
    and some visitors may or may not \emph{modify} the nodes.
Therefore, the visitor is parameterized on line~\ref{Visitor:start} by the owner (\code{NodeO}) and
    immutability (\code{NodeI})
    of the nodes.
The \code{visit} method on line~\ref{Visitor:visit} is mutable because it changes the visitor
    that accumulates information during the traversal.
%
%
%
%
%
%
%
Different visitor implementations may have different immutability for the nodes,
    e.g., readonly on line~\ref{Visitor:visit:ReadOnly} or mutable
    on line~\ref{Visitor:visit:Mutable}.
%
%
%
%

Finally, note how the type arguments \code{\underline{This,ReadOnly}} of the
    node on line~\ref{Visitor:match1:ReadOnly}
    match the last two arguments of the visitor
    on line~\ref{Visitor:match2:ReadOnly},
    and on line~\ref{Visitor:match1:Mutable} the type
    arguments~\code{\underline{This,Mutable}}
    match those on line~\ref{Visitor:match2:Mutable}.
%
%
This shows that the same \code{accept} method
    (without duplicating the nodes' hierarchy traversal code)
    can be used both for readonly and mutable hierarchies.

%
%
%
%
%
%
%
%



\Section[formal]{Formalization and Type Soundness}
Proving soundness is essential in the face of complexities
    such as wildcards and raw/cooked objects.
This section gives the typing rules and operational semantics of a simplified version of OIGJ
    and sketches the proofs of our immutability and ownership guarantees.
For lack of space, the full proofs are included in our technical report~\cite{ZibinUpdated2010}.

%

Our type system, called Featherweight OIGJ (FOIGJ),
    is based on Featherweight Java (FJ)~\cite{Igarashi:2001:FJM}.
FOIGJ models the essence of OIGJ:
    the fact that every object has an ownership and immutability,
    and the cooking phase when creating immutable objects.
FOIGJ adds imperative constructs to FJ,
    such as \code{null} values, field assignment, locations/objects, and a heap.
FOIGJ also adds a constructor body (to model the cooking phase),
    owner and immutability parameters to classes,
    guards as in cJ~\cite{HuangZS2007:cJ},
    wildcard owners,
    and the run-time notion of raw/cooked objects.


FOIGJ poses two main challenges:
    (i)~modeling \emph{wildcards} in the typing rules,
    and (ii)~the representation for \emph{raw objects}.
We use the following example (similar to \Ref{Figure}{OIGJ-example}) to demonstrate these two challenges:
\begin{algorithmic}
\STATE \code{class Foo<O,I> \lb}
\STATE \code{~Date\hgn{{O},{I}} sameD;}
\STATE \code{~Date\hgn{{\This},I} ownedD;}
\STATE \code{~Date\hgn{{\This},Immut} immutD;}
%
\STATE \code{~\underline{<I extends Raw>?} void Foo()\lb}
\STATE \code{~~~this.ownedD = new Date\hgn{This,\underline{I}}();}
\STATE \code{~~~this.immutD = new Date\hgn{This,\underline{Immut}}();}
\STATE \code{~~~\ldots~\rb~\rb}
%
%
%
\end{algorithmic}

Wildcards pose a difficulty due to a process in Java called \emph{wildcard capture} in which
    a wildcard is replaced with a fresh type variable.
For example, the two underlined wildcards below might represent two distinct owners:
\begin{algorithmic}
\STATE \code{Foo<\underline{?},I> f = \ldots;}
\STATE \code{Date<\underline{?},I> d = \ldots;}
\STATE \code{f.sameD = d;} \myCOMMENT{Illegal assignment! Different owners! } %
\end{algorithmic}
A Java compiler rejects the assignment
    due to incompatible types, because the wildcards were captured by different type variables.
Formalizing the full power of wildcards (with upper and lower bounds)
    was only recently achieved~\cite{CameronDE2008}.
FOIGJ does \emph{not} model wildcard capture.
Instead, it is enough to augment
    the field assignment rule
    with the following check:
    assigning to~$o$ is illegal if~$\Ofn{o}=\code{?}$ (similarly for method invocation).
This extra check is needed only in FOIGJ, and not in OIGJ, because OIGJ is built on top of Java, which supports wildcard capture.
%

The second challenge is modeling raw objects in the \emph{non-erased} operational semantics.
Recall that generics are erased in Java and are not present at run time.
FOIGJ's \emph{erased} operational semantics is identical to that of normal Java:
    ownership and immutability information is not kept.
In contrast, the \emph{non-erased} version stores with each object its owner and immutability,
    and it checks at run time the ownership and immutability guarantees
    (i.e., that field assignment respects owner-as-dominator and
    is done only on mutable or raw objects).
The non-erased version is used only in the formalism.
    Storing the owner and immutability of every object at run time would be
a huge overhead, and is not required for correctness if the program
satisfies OIGJ's type rules.

The non-erased semantics of Featherweight Generic Java~\cite{Igarashi:2001:FJM} (FGJ)
    performs variable substitution for method calls,
    however FGJ's way of doing substitution does not work in FOIGJ.
For example, consider the following reduction as done in imperative FGJ: %
\begin{algorithmic}
\STATE $\code{new Foo<World,\underline{Immut}>()} \reducesto$
\STATE ~~~~~~~~~~~~~~~~~~~~~~~~~~~$\code{~l.ownedD = new Date\hgn{l,\underline{Immut}}();}$
\STATE ~~~~~~~~~~~~~~~~~~~~~~~~~~~$\code{~l.immutD = new Date\hgn{l,\underline{Immut}}();}\ldots$
\end{algorithmic}
The variable \hI in the constructor was substituted with \Immut,
    and the variables \this and \This were substituted with a new location~\hl
    that was created on the heap,
    i.e., the heap~$H$ now contains a new object  in location~\hl whose fields are all \code{null}:~~
    $H = \{ \hl \mapsto \code{Foo<World,Immut>(}\ol{\code{null}}\code{)} \}$.
(Locations are pointers to objects; we treat locations and objects identically because they have a one-to-one mapping,
    e.g., the owner of a location is defined to be the owner of its object.)
Note how owner parameters ($\Ofn{o}$) at compile time are replaced with owners ($\Owner{o}$) at run time,
    e.g., \This was replaced with location~\hl.

There are two reasons why substituting \hI with \Immut does not work in FOIGJ:
(i)~the reduction does not type-check because we mutate an immutable object (\code{l.ownedD = \ldots}),
and (ii)~we lost information about the two new \code{Date} objects,
    namely that \code{ownedD} can still be mutated after its constructor finishes (because it is \this-owned)
     whereas \code{immutD} cannot.

FOIGJ solves these two issues by introducing an auxiliary type~$\Immut_\hl$.
An object~$o$ of immutability~$\Ifn{o}=\Immut_\hl$
    becomes cooked when the constructor of \hl finishes,
    therefore we call~$\hl$ its \emph{cooker}, denoted by~$\Cooker{o}=\hl$.
Phrased differently, an object is cooked when its cooker is \emph{constructed} (i.e., the cooker's constructor finishes).
Note that the cooker~$\hl$ can be~$o$ itself, its owner, or even some other incomparable object.

The connection between the cooker and the owner will be shown in the subtyping and typing rules below.
Intuitively, for a reference of type~$\code{C<o,Immut}_\hl\code{>}$,
    if the cooker~\hl is not inside the owner~\ho, then that reference must point to an object whose cooker is~\hl.
Otherwise (if~\hl is inside~\ho), then that reference might point to any cooked immutable object (even one with a cooker that is not~\hl).

%
%
%
%
In our example,
    the location~\hl that was created with \code{new Foo<World,\underline{Immut}>()}
    becomes cooked when it is constructed, i.e.,~$\Cooker{\hl}=\underline{\hl}$, and
    $H = \{ \hl \mapsto \code{Foo<World,Immut}_{\underline{\hl}}\code{>(}\ol{\code{null}}\code{)} \}$.
Now FGJ's way of doing the substitution works for FOIGJ,
    because \hI is replaced with~$\Immut_\hl$,
    i.e.,\\
    $\code{~l.ownedD = new Date<l,}\underline{\Immut_\hl}\code{>();}$\\
    $\code{~l.immutD = new Date\hgn{l,\underline{Immut}}();}$\\
Note how the cooker of \code{ownedD} is~\hl,
    whereas the cooker of \code{immutD} is \code{immutD} itself.
Therefore, \code{ownedD} has a longer cooking phase than \code{immutD}.

FOIGJ also maintains
    the set of currently executing constructors~$K$, where~$K \subseteq \dom{}(H)$.
We maintain the invariant that a location~\hl is \emph{raw} iff~$\Cooker{\hl} \in K$,
    and require that \emph{only mutable or raw objects can be mutated}.
Specifically,~$\Immut_\hl$ is a subtype of \Raw when~$\hl \in K$,
    and it is a subtype of \Immut when~$\hl \not \in K$.

Type~$\Immut_\hl$ also helps understand the \textbf{Object creation rule} better.
Recall that an \Immut object can be created from a \Raw constructor,
    even though \Immut is not a subtype of \Raw,
    which seems to contradict \textbf{cJ's method guard rule}.
However, type~$\Immut_\hl$ is in fact a subtype of \Raw when the object is created,
    because in our typing rules we have that $\Immut_\hl \st \Raw$ iff~$\hl \in K$,
    and when an object is created, its cooker must be in~$K$.
Phrased differently, the type of an immutable object never changes (always $\Immut_\hl$),
    but during the program execution the set $K$ changes, and therefore the subtyping relation changes:
    initially $\Immut_\hl$ is a subtype of \Raw, but later the object becomes cooked,
    and then $\Immut_\hl$ is no longer a subtype of \Raw, but instead it becomes a subtype of~$\Immut$.


\begin{figure*}[htpb!]
\begin{center}
\begin{tabular}{|l|l|}
\hline

$\code{FT} ::= \hC\hgn{\code{FO},\code{IP}}$ & Field (and method return) Type. \\

$\code{T} ::= \hC\hgn{\code{MO},\code{IP}}$ & Type. \\

$\code{N} ::= \hC\hgn{\code{NO},\code{NI}}$ & Non-variable type (for objects). \\

$\code{NO} ::= \World ~|~ \colorbox{light}{\hl}$ & Non-variable Owner parameter (for objects). \\

$\code{FO} ::= \code{NO} ~|~ \This ~|~ \hO$ & Field Owner parameter. \\

$\code{MO} ::= \code{FO} ~|~ \code{?}$ & Method Owner parameter (including generic wildcard). \\

$\code{NI} ::= \Mutable ~|~ \colorbox{light}{$\Immut_\hl$}$ & Non-variable Immutability parameter (for objects). \\

$\code{VI} ::= \code{NI} ~|~ \Immut ~|~ \hI$ & Variable Immutability for \code{new}. \\

$\code{IP} ::= \ReadOnly ~|~ \code{VI}$ & Immutability Parameter. \\

$\code{IG} ::= \ReadOnly ~|~ \Immut ~|~ \Mutable ~|~ \Raw$ & Immutability method Guard. \\

$\hM ::= \code{<I extends IG>?} ~ \code{FT} ~ \hm\hparen{\ol{\code{T}} ~ \ol{\hx}} ~ \lb\ \hreturn ~ \he\texttt{;}~\rb$
& Method declaration. \\

$\hL ::= \hclass ~ \hC\hgn{\hO,\hI}\code{~extends~C'}\hgn{\hO,\hI} \lb\ \ol{\code{FT}}~\ol{\hf}\texttt{;} \ol{\hM}~\rb$
& cLass declaration. \\

%
%
%

$\hv ::= \code{null} ~|~ \colorbox{light}{\hl} $
& Values: either \code{null} or a location~\hl. \\


%
$\he ::= \hv ~|~ \hx ~|~ \he.\hf ~|~ \he.\hf = \he ~|~ \he.\hm\hparen{\ol{\he}} ~|~ \hnew ~ \hC\hgn{\code{FO},\code{VI}}\hparen{\ol{\he}}  ~|~ \colorbox{light}{\he\code{;return l}}$
& Expressions. \\ %

\hline
\end{tabular}
\end{center}
\caption{FOIGJ Syntax. The terminals are \code{null},
    owner parameters~(\hO, \This, \World),
    and immutability parameters~(\hI, \ReadOnly, \Mutable, \Raw, \Immut).
    Given a location~\hl, $\Immut_\hl$ represents an immutable object with cooker~\hl.
    The program source code cannot contain the grayed elements (locations are only created during execution/reduction in \RULE{R-New} of \Ref{Figure}{reduction}).
    }
\label{Figure:syntax}
\end{figure*}


Faced with such major challenges,
%
    we removed from FOIGJ anything that was not needed to prove our run-time guarantees.
Specifically, FOIGJ does \emph{not} model:
    generics (except for the owner and immutability parameters),
    owner polymorphic methods, casting, inner classes, fresh owners,
    or multiple immutability/owner parameters.
On the one hand, the interaction between generics and \emph{immutability} (which enables covariant subtyping)
    was previously proven sound in Featherweight IGJ (FIGJ)~\cite{ZibinPAAKE2007}.
On the other hand, the interaction between generics and \emph{ownership} (as found in the ownership nesting rule)
    was previously proven sound in Featherweight OGJ (FOGJ)~\cite{PotaninNCB2006}.
Because covariant subtyping (as found in IGJ) and ownership nesting (as found in OGJ) was not changed in OIGJ,
    we decided not to model generics in FOIGJ.
We note that FOIGJ does model \Raw, which was not modeled previously in FIGJ.


Consider the typing rules in \Ref{Figure}{oigj-typing-rules}.
Classes in FOIGJ have a single \Raw constructor,
    therefore \textbf{Object creation rule} is always satisfied and can be ignored.
Furthermore, because FOIGJ does not model generics, static, or inner classes,
    then the following rules can also be ignored:
        \textbf{Ownership nesting}, \textbf{Inner classes}, \textbf{Inheritance},
        \textbf{Invariant}, \textbf{Erased signature},
        and
        \textbf{Fresh owners}.
Covariant subtyping and erased signatures were described in FIGJ,
    and ownership nesting and (limited) owner-polymorphic methods in FOGJ.
We stress that FOIGJ \emph{does} model wildcard for the owner parameter (\code{?}), %
    which is used in owner-polymorphic methods such as \code{sort} or \code{equals}.
In our view, extending the formalism with fresh owners or inner classes
    increases the complexity of the calculus without providing new insights.
%

The following rules are enforced by the syntax of FOIGJ (\Ref{Figure}{syntax}):
    \textbf{Generic Wildcards} and
    \textbf{\Raw parameter}.
The remaining rules are:
    \textbf{Field assignment},
    \textbf{Field access},
    \textbf{Method invocation},
    \textbf{cJ's~\cite{HuangZS2007:cJ} method guard},
    and a \textbf{Subtype relation} (without generics).
These rules are formalized in FOIGJ in the subtyping rules of \Ref{Figure}{subtyping} ($\KGdash \hT \st \code{T'}$)
    and the typing rules of \Ref{Figure}{expressions} ($\KGdash \he:\hT$).
Finally, the reduction rules are described in \Ref{Figure}{reduction} ($K \vdash H,\he \reducesto H',\he'$).


\Ref{Section}{syntax} describes the syntax of FOIGJ,
    \Ref{Section}{subtyping} the subtyping rules,
    \Ref{Section}{type-checking} the typing rules,
    \Ref{Section}{reduction} the reduction rules,
    and \Ref{Section}{soundness} proves preservation, progress, and our run-time immutability and ownership guarantees.



\Subsection[syntax]{Syntax of FOIGJ}
FOIGJ adds imperative extensions to FJ such as assignment to fields, object locations, \code{null}, and
    a heap~\cite{pierce:2002:types-and-pls}.
A constructor initializes all the fields to \code{null},
    and then calls a \code{build} method that constructs the object.
Having \code{null} values is important because \this-owned fields must be initialized with \code{null}
    since they cannot be assigned from the outside,
    i.e., they must be created within \this.
For example, a list constructor cannot receive its entries as constructor arguments;
    instead it must create the entries within the \code{build} method.

\Ref{Figure}{syntax} presents the syntax of FOIGJ.
Expressions in FOIGJ include the four expressions in FJ
    (method parameter, field access, method invocation, and new instance creation; \emph{without} casting),
    as well as the imperative extensions (field update,~$\he\code{;return l}$, and values).
Expression~$\code{e;return l}$ is created when reducing a constructor call,
    e.g., $K \vdash \code{new N(\ldots)} \reducesto \code{l.build(\ldots);return l}$,
    then we proceed to reduce~$\code{l.build(\ldots)}$ and finally return \hl.
Note that \hO and \hI are terminals, i.e.,
    the owner and immutability parameters are always named~\hO and \hI.

An evaluation of an expression (\he)
    is either infinite,
    or is stuck on \code{null}-pointer exception,
    or terminates with a value (\hv), which is either \code{null} or a location~\hl.



\begin{figure*}[!bt]
\begin{center}
\begin{tabular}{|c|}
\hline


$\typerule{
}{
  \KGdash \hI \st \Gamma(\hI)
}$~\RULE{(S1)}\quad


$\typerule{
}{
  \KGdash \hT \st \hT
}$~\RULE{(S2)}\quad

$\typerule{
  \KGdash \code{S} \st \hT
   \gap
  \KGdash \hT \st \hU
}{
  \KGdash \code{S} \st \hU
}$~\RULE{(S3)}\quad
$\typerule{
  \code{class C<O,I> extends C}'\code{<O,I>}
}{
  \KGdash \hC\hgn{\code{MO},\code{IP}} \st \code{C}'\hgn{\code{MO},\code{IP}}
}$~\RULE{(S4)}

\\


$\typerule{
}{
  \KGdash \Mutable \st \Raw
}$~\RULE{(S5)}\quad
$\typerule{
}{
  \KGdash \Raw \st \ReadOnly
}$~\RULE{(S6)}\quad
$\typerule{
}{
  \KGdash \Immut \st \ReadOnly
}$~\RULE{(S7)}
 \\

$\typerule{
    \KGdash \code{IP} \st \code{IP}'
}{
  \KGdash \hC\hgn{\code{MO},\code{IP}} \st \hC\hgn{\code{MO},\code{IP}'}
}$~\RULE{(S8)}\quad
$\typerule{
}{
  \KGdash \hC\hgn{\code{MO},\code{IP}} \st \hC\hgn{\code{?},\code{IP}}
}$~\RULE{(S9)}
\quad
$\typerule{
\hl \in K
}{
  \KGdash \Immut_\hl \st \Raw
}$~\RULE{(S10)}
\\
$\typerule{
\hl \not \in K
}{
  \KGdash \Immut_\hl \st \Immut
}$~\RULE{(S11)}
\quad
$\typerule{
\hl \not \in K
}{
  \KGdash \Immut \st \Immut_\hl
}$~\RULE{(S12)}
\quad
$\typerule{
\hl \OprecNotEqual \code{NO}
}{
  \KGdash \hC\hgn{\code{NO},\Immut} \st \hC\hgn{\code{NO},\Immut_\hl}
}$~\RULE{(S13)}
\\

\hline
\end{tabular}
\end{center}
\caption{FOIGJ Subtyping Rules ($\KGdash \hT \st \code{T'}$). Rule~\RULE{S13} shows the connection between cooker~\hl and owner~\code{NO}.}
\label{Figure:subtyping}
\end{figure*}


Note how the syntax limits the usage of wildcards and \Raw:
    wildcards (\code{?}) can be used only as the owner of method arguments (FOIGJ does not have local variables),
    and \Raw only as a method guard (\code{IG}).

We represent sequences using an over-line notation, similarly to FJ, i.e.,
    comma denotes concatenation of sequences,
    and
    $\ol{\code{FT}}~\ol{\hf}\texttt{;}$ represents
    the sequence~$\code{FT}_1~\hf_1\texttt{;}\ldots\code{FT}_n~\hf_n\texttt{;}$

A class in FOIGJ has a single constructor that can create both mutable and immutable objects,
    i.e., it is a \Raw constructor.
The constructor is not shown in the syntax because it can be inferred from the class declaration:
    it always assigns \code{null} to the fields of the newly created object,
    and then invokes this special method (ignoring the return value):\\
\code{<I extends Raw>? \code{T'} build($\ol{\code{T}}~\ol{\he}$) \lb{}~return e; \rb}\\ %
We require that each class has such a method,
    and that its parameters are not \this-owned nor have wildcards.
The reduction rules call that method after the fields are set to \code{null}.




\Subsection[subtyping]{Subtyping in FOIGJ}


An environment~$\Gamma$ is a finite mapping from variables~\hx and locations~\hl to types~\hT,
    e.g.,~$\hx:\hT \in \Gamma$.
The location types define the ownership tree~$\Oprec$ (or without reflexivity~$\OprecNotEqual$).
The set of currently executing constructors is denoted~$K$.
In addition,~$\Gamma$ maps the immutability parameter~\hI to its bound according
    to the current method's guard (\code{IG} in \Ref{Figure}{syntax}).
For example,~$\hI:\Raw \in \Gamma$ when typing the expression \he in method \code{build} above.
%


\Ref{Figure}{subtyping} shows FOIGJ subtyping rules.
Rules~\RULE{S1}--\RULE{S4} are the same as FGJ rules:
    \RULE{S1} means that a generic variable is a subtype of its bound,
    \RULE{S2} is reflexivity, \RULE{S3} is transitivity, and \RULE{S4} is that subclassing defines subtyping.
Rules~\RULE{S5}--\RULE{S7} show subtyping among non-variable immutability parameters
    as shown in \Ref{Figure}{owners-and-immutability-params}b.
Rule~\RULE{S8} defines covariant subtyping for the immutability parameter.
Rule~\RULE{S9} formalizes subtyping with a wildcard owner.

The last four rules \RULE{S10}--\RULE{S13}
    are concerned with \emph{cookers} such as~$\Immut_\hl$.
Recall that an object is cooked when its cooker~\hl is constructed,
    i.e., the constructor of~\hl is no longer executing:~$\hl \not \in K$.
Rule~\RULE{S10} views the type as \Raw, while rules~\RULE{S11}--\RULE{S12} shows the equivalence to \Immut.
Note that subtyping is no longer antisymmetric,
    i.e., there are non-equal types~$\hT_1$ and~$\hT_2$ for which~$\hT_1 \st \hT_2 \st \hT_1$.
For example,~$\hT_1=\code{C<O,Immut}_{\code{l}}\code{>}$ and~$\hT_2=\code{C<O,Immut>}$,
    when~$\code{l} \not \in K$.
In fact, this is not surprising because these types both represent immutable object,
    and after the cooker is cooked, the identity of the cooker is irrelevant.

\paragraph{Cooker vs.\ owner}
Rule~\RULE{S13} assumes that the cooker is inside the owner ($\hl \OprecNotEqual \code{NO}$),
    which means the object might came from the outside.
This rule addresses the difference between the cooker of (i)~a location~\hl
    or (ii)~that of an expression such as field access~\code{l.f}:
    (i) location~\hl will be cooked \emph{exactly} when the constructor of~$\Cooker{\hl}$ is finished, however,
    (ii) the cooker of~\code{l.f} is an \emph{over-approximation}, i.e.,
        the object stored in that field might have been cooked earlier.
Rule~\RULE{S13} allows an over-approximation only when the cooker is inside the owner.

Consider this example:
\begin{algorithmic}
\STATE $\code{class Foo<O,I> \lb~Date<O,I> same;}$
\STATE $\code{~<I extends Raw>? Foo(Date<O,I> d) \lb{}~same=d;~\rb~~\rb}$
\end{algorithmic}
Field~\code{same} is assigned from the outside, but it might still be \this-owned.
We will show the reduction of two expressions: one where \code{same} is assigned a cooked (outside) date,
    and one with a raw date.
The expressions are inside the constructor of some object~\code{b}
    whose cooker is~\code{b} itself.

The reduction of the first expression:
\begin{algorithmic}
\STATE \code{new Foo<This,Immut>(new Date<This,Immut>())}
\end{algorithmic}
results in the heap:
$H=\{
\code{d1} \mapsto \code{Date<b,Immut}_{\code{d1}}\code{>()} ,
\code{f1} \mapsto \code{Foo<b,Immut}_{\code{f1}}\code{>(d1)}
%
\}$.
Note that the type of~\code{d1} must be a subtype of \code{f1.same}
    in a well-typed heap (formally defined later).
The type of~\code{d1} is a subtype of \code{Date<b,Immut>}
    (because $\code{d1} \not\in K$ in rule~\RULE{S12}),
    which is a subtype of $\code{Date<b,Immut}_{\code{f1}}\code{>}$
    (because $\code{f1} \OprecNotEqual \code{b}$ in rule~\RULE{S13}).
Phrased differently, the cooker of \code{f1.same} is \code{f1},
    but it may point to an object that was cooked before,
    and indeed it points to an object whose cooker is \code{d1}
    (so it is an over-approximation).


The reduction of the second expression:
\begin{algorithmic}
\STATE \code{new Foo<This,I>(new Date<This,I>())}
\end{algorithmic}
results in the heap (because~$\hI=\code{Immut}_{\code{b}}$):
$H=\{
\code{d2} \mapsto \code{Date<b,Immut}_{\code{b}}\code{>()} ,
\code{f2} \mapsto \code{Foo<b,Immut}_{\code{b}}\code{>(d2)}
\}$.
Note that in this case, both~\code{d2} and~\code{f2} have the same cooker~\code{b}.
The type of \code{f2.same} is $\code{Date<b,Immut}_{\code{b}}\code{>}$,
    and because $\code{b} \not \OprecNotEqual \code{b}$ (see rule~\RULE{S13}),
    then we know that this is not an over-approximation,
    i.e., that field points to an object whose cooker must be \code{b}.

To summarize, consider a type $\code{Foo<o,Immut}_{\code{c}}\code{>}$.
If the cooker~\code{c} is inside the owner~\code{o} ($\code{c} \OprecNotEqual \code{o}$),
    or the cooker is cooked ($\code{c} \not \in K$),
    then the type is an over-approximation,
    i.e., it can point to any \Immut object (that is, to any object with cooker~$\code{c'} \not\in K$).
Otherwise, it points to an object whose cooker is exactly~\code{c}.
Formally,
\begin{Lemma}[Exact-Cooker]
If $\KGdash \code{C<MO,IP>} \st \code{C'<NO,Immut}_{\hl}\code{>}$,
    $\hl \not\OprecNotEqual \code{NO}$, and $\hl \in K$,
    then~$\code{IP}=\code{Immut}_{\hl}$.
\end{Lemma}

We also prove in the technical report that:
\begin{Lemma}[Owners-Invariant]
If $\KGdash \code{C<MO,IP>}\st\code{C'<MO',IP'>}$, then
    (i)~$\code{MO'}\neq\code{?} \Rightarrow \code{MO}=\code{MO'}$,
    (ii)~$(\code{IP'}\neq\Immut_\hl \text{~or~} \hl \not\OprecNotEqual \code{MO'}) \Rightarrow \KGdash \code{IP} \st \code{IP'}$, and
    (iii)~\code{C} is a subclass of~\code{C'},
    (iv)~$\KGdash \code{D<l,IP>}\st\code{D<l,IP'>}$ for any class~\code{D} and location~\hl where~$\code{MO'} \Oprec \hl$.
\end{Lemma}

%
%
%
%
%
%
%


\Subsection[type-checking]{Typing rules of FOIGJ}


\begin{figure*}[t]
\begin{center}
\begin{tabular}{|c|}
\hline
$\typerule{
  K \cup \{ \hl \},\Gamma \vdash \he:\hT
}{
  \KGdash \code{e;return l} : \Gamma(\hl)
}$~\RULE{(T-return)}
\quad
$\typerule{
  \mtype{}(\bot,\code{build},\code{C<FO,VI>})=\ol{\code{T}}\rightarrow\code{U}
    \gap
  \KGdash \ol{\he}:\ol{\code{T'}}
    \gap
  \KGdash \ol{\code{T'}} \st \ol{\code{T}}
}{
  \KGdash \code{new C<FO,VI>(}\ol{\he}\code{)} : \code{C<FO,VI>}
}$~\RULE{(T-New)}\\\\

$\typerule{
}{
  \KGdash \hx : \Gamma(\hx)
}$~\RULE{(T-Var)}
\quad
$\typerule{
}{
  \KGdash \code{null} : \hT
}$~\RULE{(T-null)}
\quad
$\typerule{
  \KGdash \he:\code{C<MO,IP>}
    \gap
  \ftype{}(\he,\hf,\code{C<MO,IP>})=\hT
}{
  \KGdash \he.\hf : \hT
}$~\RULE{(T-Field-Access)}\\\\

$\typerule{
}{
  \KGdash \hl : \Gamma(\hl)
}$~\RULE{(T-Location)}
\quad
$\typerule{
  \KGdash \he.\hf : \hT
    \gap
  \KGdash \code{e'}:\code{T'}
    \gap
  \KGdash \code{T'} \st \hT
    \gap
  \KGdash \he:\code{C<MO,IP>}
    \\
  \KGdash \code{IP} \st \Raw
    \gap
  \isTransitive(\he,\Gamma,\code{C<MO,IP>})
    \gap
  \code{MO} \neq \code{?}
}{
  \KGdash \he.\hf = \code{e'} : \code{T'}
}$~\RULE{(T-Field-Assignment)}\\\\

$\typerule{
  \KGdash \he_0:\code{C<MO,IP>}
    \gap
  \mtype{}(\he_0,\hm,\code{C<MO,IP>})=\ol{\code{T}}\rightarrow\code{T"}
    \gap
  \KGdash \ol{\he}:\ol{\code{T'}}
    \gap
  \KGdash \ol{\code{T'}} \st \ol{\code{T}}
    \gap
  \mguard{}(\hm,\code{C})=\code{IG}
    \\
  \KGdash \code{IP} \st \code{IG}
    \gap
  \code{IG}=\Raw \Rightarrow \isTransitive(\he_0,\Gamma,\code{C<MO,IP>})
    \gap
  \mtype{}(\hm,\code{C})=\ol{\code{U}}\rightarrow\code{V}
    \gap
  \Ofn{\code{T}_i}=\code{?} \Rightarrow \Ofn{\code{U}_i}=\code{?}
}{
  \KGdash \he_0\code{.m(}\ol{\he}\code{)} : \code{T"}
}$~\RULE{(T-Invoke)}\\


\hline
\end{tabular}
\end{center}
\caption{FOIGJ Expression Typing Rules ($\KGdash \he:\hT$).} %
\label{Figure:expressions}
\end{figure*}


%
\paragraph{Auxiliary functions}
We use the following auxiliary functions:
    $\fields{}(\hC)$ returns all the field names (including inherited fields) of class~\hC,
    $\ftype{}(\hf,\hC)$ returns the type of field~\hf in class~\hC,
    $\mtype{}(\hm,\hC)$ returns the type of method~\code{m} in class~\hC,
    and $\mbody{}(\hm,\hC)$ returns its body.
Their definitions are based on their counterparts in FJ, and thus omitted from this paper.
In addition, function
    $\mguard{}(\hm,\hC)$ returns the method's guard (\code{IG} in \Ref{Figure}{syntax}).

We overload the auxiliary functions above to work also for types ($\hT=\code{C<MO,IP>}$) and not just classes (\hC)
    by substituting~\code{$[$MO$/$O$,$IP$/$I$]$}.
However, we also need to carefully substitute \This when the receiver is \this or locations.
Function~$\ftype{}(\underline{\he},\hf,\hT)$ returns the type of the field access~\code{\underline{e}.f}
    where \hT is the type of~\he, or \code{error} if the access is illegal.
For example,
\beqst
\code{\ftype{}(ownedD,Foo)} & = \code{Date<This,I>} \\
\code{\ftype{}(\this,ownedD,Foo<O,Immut>)} & = \code{Date<This,Immut>}\\
\code{\ftype{}(\this.f,ownedD,Foo<O,Immut>)} & = \code{error}\\
\code{\ftype{}(l,ownedD,Foo<o,Immut}_\hc\code{>)} & = \code{Date<l,Immut}_\hc\code{>}\\
\eeq
Formally, \code{\ftype{}(e,f,C<MO,IP>)=$[$MO$/$O$,$IP$/$I$,$z$/$This$]$\ftype{}(f,\hC)},
    where (i)~$\code{z}=\hl$ if~$\he=\hl$, (ii)~$\code{z}=\This$ if~$\he=\this$, (iii)~otherwise~$\code{z}=\code{error}$
    (and if a type contains \code{error} then it means the call to $\ftype$ failed).
When we know the field is not \this-owned, then the expression~\he is not used,
    and we write~$\ftype{}(\bot,\hf,\hC)$.
However, if the field is \this-owned, then~\he must be \this or a location~\hl.

Recall that \textbf{Field access rule} in \Ref{Figure}{oigj-typing-rules}
    required that
    \this-owned fields can be accessed only via \this.
At run time, \this is substituted with a location~\hl.
Therefore, there is a \emph{duality} between \this and a location~\hl in the definition of~\ftype.
For example, the field access \code{\underline{this}.ownedD} of type \code{Date<\underline{This},I>}
    is legal because we accessed a \this-owned field via \underline{\this}.
At run time, \this is substituted with some location~\hl,
    and the access \code{\underline{l}.ownedD} of type \code{Date<\underline{l},\ldots>} is now still legal because
    we accessed a \this-owned field via \underline{a location~\hl}.
Note that if the access is not done via a location, e.g., \code{bar.l.ownedD},
    then we cannot type-check the resulting expression (because we do not know what should be the substitute for \This).

There is a similar duality
    in \textbf{Field assignment rule} part (ii),
    that checks that \Raw is transitive for \this or \this-owned objects.
The dual of \this is a location~\hl,
    and the dual of a \this-owned object (\code{C<This,I>})
    is an object whose cooker is not inside its owner ($\code{C<o,Immut}_\hl\code{>}$ where~$\hl \not \OprecNotEqual \code{o}$).
The second duality holds because, for type \code{C<This,I>}, the cooker (\hI) is never inside the owner (\This).
At run time, the owner will be the location of \this,
    and the cooker is either \this or some other object that was created before \this,
    i.e., the cooker is never inside the owner (but they might be equal).

Function~\isTransitive{} checks whether \Raw is transitive.
The underlined part shows the \emph{dual} version of \textbf{Field assignment rule} part (ii):
    (i)~\this vs.~$\hl'$,
    and (ii)~$\code{MO}=\This$ vs.~$\hl \not \OprecNotEqual \code{MO}$.

\begin{algorithmic}
\STATE $\isTransitive{}(\he,\Gamma,\code{C<MO,IP>})~=$
\STATE $~~\big(\code{IP}=\hI \text{~and~} \Gamma(\hI)=\Raw \Rightarrow (\code{e=\this{}}\text{~or~~}\code{MO}=\This)\big)\text{~or~}$
\STATE $~~\gap~~~ \big(\underline{\code{IP}=\Immut_\hl \Rightarrow (\code{e=l'}\text{~or~}\hl \not \OprecNotEqual \code{MO})}\big)$
%
\end{algorithmic}



\paragraph{Typing class declarations}
FOIGJ program consists of class declarations followed by the program's expression.
Next, we describe in words the rules for typing the class declarations,
    and the rules for typing an expression are given formally in \Ref{Figure}{expressions}.
When typing an expression, we assumed the class declarations are well-formed.

To check that class declarations are well-formed, FOIGJ first
    performs all the checks done in FJ,
    e.g., that there are no cycles in the inheritance relation,
    that field and method names are unique in a class,
    that \this is not a legal method parameter name,
    that an overriding method maintains the same signature, etc.
FOIGJ performs additional checks related to method guards when typing method declarations,
    i.e., we modify rule \formalrule{T-Method} in FJ as follows:
    (i)~An overriding method can only make the guard weaker,
        i.e., if a method with guard \code{IG} overrides one with guard \code{IG'}
            then~$\code{IG'} \st \code{IG}$.
    (ii)~In class~\hC, when typing a method:
        $\code{<I extends IG>?} ~ \code{FT} ~ \hm\hparen{\ol{\code{T}} ~ \ol{\hx}} ~ \lb\ \hreturn ~ \he\texttt{;} \rb$\\
        we use an environment~$\Gamma$ in which the bound of~\hI is \code{IG},
        i.e.,~$\Gamma=\{\hI:\code{IG}, \ol{\hx}:\ol{\code{T}}, \this:\code{C<O,I>}\}$,
        and we must prove that~$\emptyset,\Gamma \vdash \he:\code{S}$
        and~$\emptyset,\Gamma \vdash \code{S} \st \code{FT}$.
    Finally, we require that if~$\code{IG}=\ReadOnly$ then~$\Ifn{\hT_i}\neq\hI$.
This last requirement is not really a limitation, because
    a programmer can replace \hI with \ReadOnly for parameters in readonly methods,
    and previously legal programs would remain legal.
(This requirement is needed to prove preservation for the congruence rule of method receiver,
    see our technical report for details.)



\begin{figure*}[t]
\begin{center}
\begin{tabular}{|c|}
\hline

$\typerule{
  \hl \not \in \dom(H)
    \gap
  \code{VI}' =
    \begin{cases}
    \Immut_\hl & \text{if~}\code{VI}=\Immut \text{~or~} (\code{VI}=\Immut_{\hc} \text{~and~} \hc \not \in K) \\
    \code{VI} & \text{otherwise} \\
    \end{cases}
}{
  K \vdash H,\code{new C<NO,VI>}\hparen{\ol{\hv}} \reducesto H[\hl \mapsto \code{C<NO,VI'>}\hparen{\ol{\code{null}}}],\hl\code{.build}\hparen{\ol{\hv}}\code{;return l}
}$~\RULE{(R-New)}\\\\


$\typerule{
  K \cup \{\hl\} \vdash H,\he \reducesto H',\code{e'}
}{
  K \vdash H,\code{e;return l} \reducesto H',\code{e';return l}
}$~\RULE{(R-c1)}
\quad
$\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ol{\hv}}
    \gap
  \fields{}(\hC)=\ol{\hf}
}{
  K \vdash H,\hl.\hf_i \reducesto H,\hv_i
}$~\RULE{(R-Field-Access)}\\\\

$\typerule{
  H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}
    \gap
  \fields{}(\hC)=\ol{\hf}
    \gap
  \code{NI}=\Mutable \text{~or~} \CookerH{\hl} \in K
    \gap
  \hv'=\code{null} \text{~or~} \hl \Oprec \OwnerH{\hv'}
}{
  K \vdash H,\hl.\hf_i = \hv' \reducesto H[\hl \mapsto \code{C<NO,NI>(}[\hv'/\hv_i]\ol{\hv}\code{)}],\hv'
}$~\RULE{(R-Field-Assignment)}\\\\


$\typerule{
}{
  K \vdash H,\code{v;return l} \reducesto H,\hl
}$~\RULE{(R-return)}
\quad
$\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ldots}
    \gap
  \mbody{}(\hm,\code{C})=\ol{\hx}.\he'
}{
  K \vdash H,\hl\code{.m(}\ol{\hv}\code{)} \reducesto H, [\ol{\hv}/\ol{\hx}, \hl/\this, \hl/\This, \code{NO}/\hO, \code{NI}/\hI]\he'
}$~\RULE{(R-Invoke)}\\


\hline
\end{tabular}
\end{center}
\caption{FOIGJ Reduction Rules ($K \vdash H,\he \reducesto H',\he'$), excluding all congruence rules except \RULE{R-c1}.} %
\label{Figure:reduction}
\end{figure*}


\paragraph{Typing expressions}
\Ref{Figure}{expressions} shows the typing rules for expressions in FOIGJ.
Most of these rules are a direct translation from \Ref{Figure}{oigj-typing-rules}.
The main challenge was handling \emph{wildcards} correctly without resulting in wildcard-capture.
Rule \RULE{T-Field-assignment} requires that $\code{MO} \neq \code{?}$,
    i.e., one cannot assign to an object with unknown owner.
Typing method parameters is similar to typing field-assignment,
    however, method parameters can have a wildcard owner whereas fields cannot
    (see the difference between \hT and \code{FT} in \Ref{Figure}{syntax}).
Thus, rule \RULE{T-Invoke} requires that
    $\Ofn{\ol{\code{T}}}=\code{?} \Rightarrow \Ofn{\ol{\code{U}}}=\code{?}$,
    i.e., if~$\hT_i = \hC\code{<?,IP>}$ then~$\code{U}_i = \hC\code{<?,IP'>}$.
I.e.,
%
%
    if the owner of $\he_0$ is unknown, then the owner of the method parameters cannot be \hO.

Rule \RULE{T-New} performs less checks compared to a method call
    (e.g., no need to check the guard, \isTransitive, nor wildcards)
    because \code{build} has several restrictions:
    its guard is \Raw and it does not contain wildcards nor \this-owned parameters.
Because \This does not appear in the signature of \code{build},
    we know that $\mtype{}$ will not use~$\bot$ in the call:
    $\mtype{}(\bot,\code{build},\code{C<FO,VI>})$.

An expression/type is called \emph{closed} if it does not contain
    any free variables (e.g., wildcards, \this, \hI, \hO, or \This),
    but it may contain \World, \ReadOnly, \Mutable, \Immut, $\Immut_\hl$ or $\hl$.
Note that the type of a closed expression is also closed.
\begin{Lemma}[closed]
If~$\KGdash \he' : \hT'$ and $\he'$ is closed and $\he'\neq\code{null}$, then $\hT'$ is closed.
\end{Lemma}
\noindent
The delicate part of the proof is showing that~$\hT'$ does not contain \This.
Note that~$\ftype$ returns a type with \This only if~$\he=\this$
    (which cannot happen since \he is closed).





\Subsection[reduction]{Reduction rules of FOIGJ}
The initial expression to be reduced is \emph{closed},
    and we guarantee that a closed expression is always reduced to another closed expression:
%
\begin{Lemma}[reduction-closed]
If~\he is closed and~$K \vdash H,\he \reducesto H',\he'$, then~$\he'$ is closed.
\end{Lemma}

The heap (or store)~$H$ maps each location~\hl to an object~$\hC\code{<NO,NI>}\hparen{\ol{\hv}}$,
    where~$\OwnerH{\hl} = \code{NO}$ is its owner,
    and $\IfnH{\hl} = \code{NI}$ is its immutability,
    and $\ol{\hv}$ are the values of its fields.
If~$\code{NI}=\Immut_{\hl'}$ then we say that its cooker is~$\CookerH{\hl} = \hl'$.
(We added the subscript $H$ to the functions that return the owner, immutability and cooker,
    in order to explicitly show the dependence on the heap.)
We define a \emph{heap-typing}~$\Gamma_H: \hl \mapsto \hT$ that gives a type to each location
    in the obvious way (simply removing the list of fields~$\hparen{\ol{\hv}}$).

The set of currently executing constructors is~$K$.
A heap~$H$ is \emph{well-typed for~$K$} if it satisfies two conditions:
(i)~Each field location is a subtype (using~$K,\Gamma_H$) of the declared field type,
    i.e., for every location~\hl, where $H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}$ and~$\fields{}(\hC)=\ol{\hf}$,
        and
        for every field~$\hf_i$, we have that either $\hv_i=\code{null}$ or
        $K,\Gamma_H \vdash \Gamma_H(\hv_i) \st \ftype{}(\hl,\hf_i,\code{C<NO,NI>})$.
(ii)~There is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\OwnerH{\hl}=\World$ or $\OwnerH{\hl} \TprecNotEqual \hl$, and $\IfnH{\hl}=\Mutable$ or $\CookerH{\hl} \Tprec \hl$.
The linear order~$\Tprec$ can order the objects according to their \emph{creation time},
    because~$\OwnerH{\hl}$ is always created before~$\hl$,
    and~$\CookerH{\hl}$ is either~\hl or created before~$\hl$.

In our technical report we prove that if $H$ is {well-typed for~$K$} then
    (a)~owner-as-dominator holds (\Ref{Lemma}{owner-as-dominator}), and
    (b)~$H$ is well-typed for any subset of~$K$ (\Ref{Lemma}{well-typed}).
Part (b) is not trivial, because the subtyping relation for a subset of~$K$ is different because raw objects become immutable.
Intuitively, during execution objects become cooked (when their cooker is removed from~$K$), and
    therefore \Ref{Lemma}{well-typed} guarantees that the heap remains well-typed when~$K$ decreases.

\begin{Lemma}[owner-as-dominator]
If heap~$H$ is well-typed for~$K$, then for every location~$\hl \in \dom{}(H)$,
    $
    \hl \mapsto \hC\code{<NO,NI>}\hparen{\ol{\hv}}
    $,
    then either~$\hv_i=\code{null}$ or~$\hl \Oprec \OwnerH{\hv_i}$.
\end{Lemma}
\begin{Lemma}[well-typed]
Given a heap~$H$ that is well-typed for~$K$,
    then for any~$S \subset K$,
    the heap~$H$ is well-typed for~$S$.
\end{Lemma}



\Ref{Figure}{reduction} presents the reduction rules in a small-step notation,
    excluding all congruence rules except \RULE{R-c1}. %

Rule \RULE{R-return} ignores the return value of \code{build} and returns~\hl.
Rule \RULE{R-Field-Access} is trivial.
Rule \RULE{R-Field-assignment} enforces our immutability guarantee (only mutable or raw objects can be mutated)
    and our ownership guarantee (owner-as-dominator, i.e.,~\hl can point to~$\hv'$ iff~$\hl \Oprec \OwnerH{\hv'}$).
Rule \RULE{R-Invoke}
    finds the method body according to the receiver,
    and substitutes all the free variables in the method body.

Rule~\RULE{R-c1} is the congruence rule for \code{e;return l}.
Note that this rule is the only place the set~$K$ is modified,
    i.e., when reducing~\he, the set of ongoing constructors is~$K \cup \{\hl\}$.
It is easy to prove that if~$K \vdash H,\he \reducesto H',\he'$ then
    $\Gamma_H \subseteq \Gamma_{H'}$.
The other congruence rules are not shown because they are trivial,
    e.g., in order to reduce a method call~$\he_0\code{.m(}\ol{\he}\code{)}$,
    we first reduce~$\he_0$ to a location, then reduce the first argument to a value, etc.

Rule \RULE{R-New} creates a new location~\hl, sets the fields to \code{null},
    sets the cooker of~\hl (\code{VI'})
    and finally calls \code{build}.
In order to build the newly created object~\hl, then it must be raw, i.e., its cooker~\code{VI'} must be in~$K$.
(Note that~\hl will be in~$K$ according to \RULE{R-c1}.) %
Therefore, if~$\code{VI}=\Immut_{\hc}$ and~$\hc \not \in K$, then we must set the cooker to~\hl.
This can happen if there is a method that returns~\code{new C<O,I>(\ldots)}
    and the receiver is a \emph{cooked} immutable object. %




\Subsection[soundness]{Guarantees of FOIGJ}
We now turn to prove various properties of FOIGJ, including preservation theorem,
    ownership and immutability guarantees, and an erasure property.
In the remainder of this section, we assume that reduction does not get stuck on \emph{null-pointer exceptions},
    i.e., the receiver/target of field access, assignment and method calls is never \code{null}.
Under this assumption,
    then~\he can always be reduced to another expression~$\he'$.

Before stating the preservation theorem,
    we need to establish a connection between~$K$ and the reduced expression~\he, which may contain~\code{return l}.
Given an expression~\he, we define~$K(\he)$ to be the set
    of all ongoing constructors in~\he, i.e., all the locations in subexpressions~\code{e';return l}.
Formally,~$K(\code{e;return l}) = K(\code{e}) \cup \{ l \}$, and for any other expression we just recurse into all subexpressions,
    e.g.,~$K(\code{e.f=e'}) = K(\code{e}) \cup K(\code{e'})$.

We will maintain the invariant that~$H$ is well-typed for~$K \cup K(\he)$.
From \Ref{Lemma}{well-typed}, then~$H$ will also be well-typed for~$K$.
Initially, we start with a closed expression~\he without any locations (therefore~$K(\he)=\emptyset$),
    an empty heap~$H$, and an empty set of constructors~$K$.

\begin{Theorem}[preservation]
  \textbf{(Progress and Preservation)}
    For every closed expression~$\he \neq \hv$, $K$, and $H$,
        if $K,\Gamma_{H} \vdash \he : \hT$ and $H$ is well-typed for~$K \cup K(\he)$,
        then there exists~$H',\he',\hT'$ such that~$K \vdash H,\he \reducesto H',\he'$,
        $H'$ is well-typed for~$K \cup K(\he')$, \hT, \hT', and $\he'$ are closed,
        $K,\Gamma_{H'} \vdash \he':\hT'$, and~$K,\Gamma_{H'} \vdash \hT' \st \hT$.
\end{Theorem}
\noindent
Proved by showing there is always (exactly) one applicable reduction rule,
    which preserves subtyping.
From \Ref{Lemma}{reduction-closed}, we know that~$\he'$ is closed,
    and from \Ref{Lemma}{closed}, we know that $\hT$ and $\hT'$ are closed.
Next we mention some highlights from the proof.
In rule~\RULE{R-return}, we have that~$K(\he') = K(\he) \setminus\{\hl\}$, but even though we shrink~$K$, we still have a well-typed heap from \Ref{Lemma}{well-typed}.
In rule~\RULE{R-Field-Assignment}, \Ref{Lemma}{owner-as-dominator} shows that the assumption $\hl \Oprec \OwnerH{\hv'}$ holds,
    and the resulting heap is well-typed for~$K \cup K(\he')$ because~$K(\he')=\{\}$ and from \RULE{T-Field-Assignment}.
In rule~\RULE{R-New}, we need to type the call~$\hl\code{.build}\hparen{\ol{\hv}}$,
    and for parameters with immutability~$\hI$, we use the subtyping rule~\RULE{S13}.

Our ownership and immutability guarantees follow directly from the reduction rules,
    because rule \RULE{R-Field-assignment} enforces them.


\Ref{Theorem}{Erasure} shows that there is no need to maintain at run time~$K$
    nor to store the owner and immutability parameter of each object.
Formally, we define an erased heap structure~$E(H)$ that maps location to objects without these parameters,
    i.e.,~$\hl \mapsto \code{C(}\ol{\hv}\code{)} \in E(H)$.
We define the erasure of an expression~$\he$,~$E(\he)$, by deleting all generic parameters,
    and define new reduction rules~$\reducesto_E$ in the obvious way.
\begin{Theorem}[Erasure]
  \textbf{(Erasure)}
If~$K \vdash H,\he \reducesto H',\he'$
    then\\
    $\gap \gap \gap\gap \gap~~~~~~K \vdash E(H),E(\he) \reducesto_{E} E(H'),E(\he')$.
\end{Theorem}

%
%



\Section[case-studies]{OIGJ Case Studies}
This section describes our implementation of OIGJ:
the language syntax (\Ref{Section}{Annotations}) and the type-checker implementation (\Ref{Section}{Implementation}).
\Ref{Section}{CaseStudy} presents our case study
    that involved annotating Sun's implementation
    of the \code{java.util} collections, and our conclusions about the
    design of the collection classes
    w.r.t.\
    %
    ownership and immutability.

The prototype OIGJ type-checker is implemented and distributed as part of the Checker Framework~\cite{PapiACPE2008}\footnote{\url{http://types.cs.washington.edu/checker-framework/}},
    which supports pluggable type systems using type annotations.


\Subsection[Annotations]{Syntax: from generics to annotations}

Whereas this paper uses generics to express ownership and immutability
(e.g., \code{Date<O,I>}), our OIGJ implementation uses Java 7's type
annotations~\cite{JSR308-2008-09-12} (e.g., \code{@O @I Date}).  Java 7's receiver annotations
play the role of cJ's guards.

%
%
%

%
%
%
%
%
%
%
%
%

%

%
%
%
%
%
%
%
%
%
%
%
%

Using annotations has the advantage of compatibility with existing
compilers and other tools.
Another advantage is the ability to use a default value, such as \code{@Mutable}.
Furthermore, it is possible to customize these defaults per class.
Defaults are not possible in generics, because a programmer must supply arguments for all
    generic parameters.

Using annotations has the disadvantage that
    some notions are no longer explicit in the syntax,
    such as transitivity, wildcards, and generic methods.
For example, compare the annotation and generic syntax:
\begin{algorithmic}
\STATE \code{class Foo~~~~~~\lb~@O @I Bar bar;~\rb}
\STATE \code{class Foo<O,I>~\lb~Bar<O,I>~ bar;~\rb}
\end{algorithmic}
Note that the type of \code{new Foo<World,Immut>().bar}
    is explicit in the generic syntax, whereas
    the annotation syntax (\code{new @World @Immut Foo().bar}) requires additional rules that mimic generics.
Use of annotations also complicates the implementation (see below).
For practical use, the compatibility benefits of using annotations outweigh
    their disadvantages.

\textbf{OIGJ's annotations} are the Cartesian product of
    owner parameters
    and immutability parameters.
Our implementation does not yet support wildcards (though in practice the
\code{@I} and \code{@O} annotations subsume most need for wildcards),
    nor classes with multiple
    owner or immutability parameters,
    such as \code{Iterator<O,\underline{ItrI,CollectionI},E>} in \Ref{Figure}{OIGJ-LinkedList}. %
(In our case study, we implemented iterators using a single immutability parameter by declaring \code{next()} as mutable.)

A class declaration can be annotated as \code{@Immut} to indicate class
    immutability, i.e., all instances are immutable and no mutable methods exist.

%
%

%
%
%
%

%
%

%
%


\Subsection[Implementation]{OIGJ implementation}

Because a pluggable type checker augments, rather than replaces, the type
system of the underlying language, the Checker Framework
permits only language extensions that are stricter than ordinary Java.
    A pluggable type system cannot relax Java's rules, as the OIGJ
    subtyping rule does.
For example,

\begin{algorithmic}
\STATE \code{\underline{@Immut} ~~~List<\underline{@Immut} ~~~\underline{Date}> ~~a;}
\STATE \code{\underline{@ReadOnly}~List<\underline{@ReadOnly}~Date> ~~b=a;} \myCOMMENT{OK}
\STATE \code{@Immut ~~~List<@Immut ~~~\underline{Object}> c=a;} \myCOMMENT{Illegal!}
\end{algorithmic}
The assignment \code{c=a} is illegal in Java and therefore in the
    Checker Framework, though it is legal in OIGJ itself.
Phrased differently, in our implementation, the covariance is limited to annotations.

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%

%
%
%

The OIGJ type-checker incorporates, extends, and in some places overrides
the IGJ checker, and adds OGJ features.  It consists of about 700 source lines of
code (of which 100 lines is Java boilerplate to define the annotations).
Most of the code handles
default and implicit types.
%
%

%
%
%

%
%
%
%
%
%


\Subsection[CaseStudy]{\normalcode{java.util} collections case study}

As a case study, we type-checked Sun's implementations of the
\code{java.util} collections (77 classes, 33,246 lines of code).
%
%
%
%
This required us to write 85 \emph{ownership-related} annotations
and 46 \emph{immutability-related} annotations in 102 lines of code
    (the lines with \texttt{new} usually contain 2 annotations).

%
%
%
%
%
%
%
%
%
%
%

%
%
%
%
%
%
%
%
%
%
%

Sun's collections are not type-safe with respect to generics
    because Java does not support generic arrays.
However, the OIGJ implementation uses type annotations, which
    can be placed on arrays as well,
    and therefore our annotated collections type-check without any errors
    with respect to ownership and immutability.

Class \code{LinkedList} in \Ref{Figure}{OIGJ-LinkedList}
    is similar in essence to Sun's implementation.
We annotated the constructors with \Raw{},
    thus allowing creation of immutable instances.
Since all instances of \code{Entry} are \this-owned,
    using \code{@This @I} as the default annotation for \code{Entry}
    meant that only three \emph{ownership-related}\footnote{%
        The other annotations are immutability-related, e.g., receiver annotations.}
    annotations were needed in \code{LinkedList}:

%
\vbox{\begin{algorithmic}
\STATE \code{\underline{@Default(\lb This.class}, I.class\rb)}
\STATE \code{static class Entry<E> \lb}
\STATE \code{~~E element; \underline{@O} Entry<E> next; \underline{@O} Entry<E> prev;}
\STATE \code{~~\ldots~\rb}
\end{algorithmic}}

Similarly, in a \code{HashMap}, both the array and the entries are \this-owned:
    \code{~~@This @I Entry[@This @I] table;}

The case study supports these conclusions:
    (i)~the collections classes are properly encapsulated (they own their representation),
    (ii)~it is possible to create immutable instances
        (all constructors are \Raw{}),
    and~(iii)~methods \code{Map.get} and \code{clone} contain design
    mistakes (see below).
%
%
We were not previously aware of these design mistakes.
We believe that if the collections were designed with ownership and immutability
    in mind, such mistakes could be avoided.


\newcommand{\ConcurrentModificationException}{\code{Concurrent\discretionary{-}{}{}Modification\discretionary{-}{}{}Exception}}

\paragraph{Immutability of method \normalcode{get}}
Let's start with a quick riddle:
    is there a \code{Map} implementation in \code{java.util}
    that might throw an exception when running the following \emph{single-threaded}
    code?

\begin{algorithmic}
\STATE \code{for (Object key : map.keySet()) \lb~map.get(key); \rb}
\end{algorithmic}
The answer is that for a map created with

\begin{algorithmic}
\STATE \code{new LinkedHashMap(100, 1, /*accessOrder=*/ true)}
\end{algorithmic}
    that contains more than one element,
    the above code throws \ConcurrentModificationException{}
    after printing one element.

Most programmers assume that \code{Map.get} is readonly,
    but there is no such guarantee in Java's specification.
%
%
%
The documentation of \code{LinkedHashMap} states:
``\emph{A special constructor is provided to create a linked hash map whose order of iteration
    is the order in which its entries were last accessed,
    from least-recently accessed to most-recently (\emph{access-order}).
%
Invoking the \code{put} or {\code{get}} method results in an access to the corresponding entry.}''

Because calling \code{get} modified the list,
    the above code threw \ConcurrentModificationException.
Phrased differently, method \code{LinkedHashMap.get} is mutable!
Because an overriding method can only strengthen the specification of the
    overridden method, \code{HashMap.get} and \code{Map.get} must be mutable as well.

%
%


\paragraph{Ownership and method \normalcode{clone}}
Method \code{clone} violates owner-as-dominator because it leaks \this-owned references
    by creating a shallow copy,
    i.e., only immediate fields are copied.
Furthermore, Sun's implementation of \code{LinkedList} assigns to \code{\underline{result}.header},
    which is a \this-owned field.
This violates \textbf{Field assignment rule} of \Ref{Section}{typing-rules}, which only permits assignment to
    \code{\underline{this}.header}.

\begin{algorithmic}
\STATE ~\myCOMMENT{The following code appears in \code{LinkedList.clone()}.}
\STATE ~\myCOMMENT{Calling \code{super.clone()} breaks owner-as-dominator because}
\STATE ~\myCOMMENT{it leaked \code{this.header} to \code{result.header}.}
\STATE \code{LinkedList result = (LinkedList) super.clone();} \label{clone:cast}
\STATE \code{\underline{result}.header = new Entry();} \myCOMMENT{Illegal in OIGJ!} \label{clone:illegal}
\end{algorithmic}

We sketch a solution that, instead of initializing the cloned \code{result}
    from \this, uses the idea of \emph{inversion of control}.
The solution has two parts.
(1)~The programmer writes a method \code{constructFrom}
    that initializes \this from a parameter.
(This is similar to a copy-constructor in \CC,
    and indeed this method should be given all the privileges of a
    constructor, such as assignment to \code{final} fields.)
(2)~The compiler automatically generates a \code{clone} method
    that first nullifies all the reference fields
    and then calls the user generated \code{constructFrom} method.
This approach enforces the ownership and immutability guarantees.


%
%
%



\Section[related-work]{Related Work}
In this section we discuss related work on ownership and immutability.
We first highlight the relationship between OIGJ and our previous work on ownership (OGJ)
    and immutability (IGJ).
%
We also survey some of the most relevant related language designs and show how OIGJ
    compares to them.


\subsection{Relationship with OGJ and IGJ}

OIGJ can be thought of as the ``cartesian product'' of OGJ and IGJ:
    OIGJ uses two type parameters to express
    ownership and immutability.
However, the delicate intricacies between ownership and immutability
    required changes to both OGJ and IGJ, making OIGJ more expressive than
    a naive combination. %



\begin{figure}[t]
\newcommand{\YEPP}[0]{+}
\newcommand{\NOPE}[0]{}
\center
\setlength{\tabcolsep}{.3\tabcolsep}
\begin{tabular}{|l|c|c|c|c|c|c|c|}
  \hline
  %
    & {OIGJ}
    & {OGJ}
    & {IGJ}
    & {GUT}
    & {UTT}
    & {IOJ}
    & {JOE$_3$}
    \\
    & {}
    & {\cite{PotaninNCB2006}}
    & {\cite{ZibinPAAKE2007}}
    & {\cite{DietlDM2007}}
    & {\cite{MullerR2007}}
    & {\cite{HaackPSS2007}}
    & {\cite{OstlundWC2008}}
    \\
  \hline
  Owner-as-dominator    & \YEPP & \YEPP & \NOPE & \NOPE & \NOPE & \YEPP & \YEPP \\
  Owner-as-modifier     & \NOPE & \NOPE & \NOPE & \YEPP & \YEPP & \NOPE & \NOPE \\
  Readonly references   & \YEPP & \NOPE & \YEPP & \YEPP & \YEPP & \NOPE & \YEPP \\
  Immutable objects     & \YEPP & \NOPE & \YEPP & \NOPE & \NOPE & \YEPP & \YEPP \\
  Uniqueness            & \NOPE & \NOPE & \NOPE & \NOPE & \NOPE & \NOPE & \YEPP \\
  Ownership transfer    & \NOPE & \NOPE & \NOPE & \NOPE & \YEPP & \NOPE & \NOPE \\
\hline
Factory method pattern  & \YEPP & \YEPP & \YEPP & \YEPP & \YEPP & \NOPE & \YEPP \\
  Visitor pattern       & \YEPP & \NOPE & \YEPP & \NOPE & \NOPE & \NOPE & \NOPE \\
Sun's \code{LinkedList} & \YEPP & \NOPE & \NOPE & \NOPE & \NOPE & \NOPE & \NOPE \\
%
  \hline
\end{tabular}
\caption{Features supported by various language designs.}
\label{Figure:Comparison}
\end{figure}


\textbf{Ownership Generic Java (OGJ)}~\cite{PotaninNCB2006} demonstrated how
    ownership and generic types can be unified as a language feature.
OGJ featured a single owner parameter for every class that was treated in the same
    way as normal generic type parameters, simplifying the language, the formalism,
    and the implementation.

OGJ completely prohibits wildcards as owner parameters, e.g., \code{Point<?>},
    whereas OIGJ relaxes this rule and allows wildcards on stack variables,
    which enables writing the \code{equals} method
    (see \textbf{Generic Wildcards rule} in \Ref{Section}{typing-rules}).

In OGJ, a method may have generic parameters that are owner parameters,
        e.g.,
        \begin{algorithmic}
        \STATE \code{class Foo<O extends World> \lb}
        \STATE \code{~<\underline{O2 extends World}> void bar(Object<\underline{O2}> o) \lb \ldots \rb}
        \end{algorithmic}
However, OGJ required that
    the parametric owners are \emph{outside}
    the owner of the class, e.g., $\code{O} \Oprec \code{O2}$.
This rule is very restrictive, however it guarantees that the ownership
    structure is a tree.
OIGJ removed this rule at the cost of complicating the
    ownership structure: it is a \emph{directed acyclic graph} (DAG) instead of a tree.

Finally, OIGJ can express temporary
    ownership within a method by using a fresh owner parameter
    (see \textbf{Fresh owners} in \Ref{Section}{typing-rules}).

\textbf{Immutability Generic Java (IGJ)}~\cite{ZibinPAAKE2007} showed
    how generic types can be used to provide support for readonly references
    and object immutability. %
OIGJ used ownership information to improve the expressiveness of IGJ.
Specifically, certain restrictions in IGJ no longer apply in OIGJ for \this-owned objects.
For example, \Raw is \emph{not} transitive in IGJ,
    e.g., the assignment to \code{next} in \Ref{Figure}{OIGJ-LinkedList}
    on lines~\ref{OIGJ:assignment:ctor1} and~\ref{OIGJ:assignment:addAll}
    is illegal in IGJ, thus limiting creation of immutable objects.
In contrast, \Raw is transitive in OIGJ for \this-owned fields (see
\textbf{Field assignment rule} in \Ref{Section}{typing-rules}),
    and therefore there was no need to refactor the collections' code.

IGJ includes an \code{@Assignable} annotation on fields that permits field assignment %
    even in immutable objects.
The \code{@Assignable} annotation indicates that a given field
%
is not part of the object's abstract state.
This is necessary to type-check caches, lazily-initialized fields, and
other programming idioms.
%
%
%
%
OIGJ removed this annotation to simplify the formalism.  This also guarantees
representation immutability as well as immutability of the abstraction:
the fields of a cooked immutable object never change.
Our implementation supports the \code{@Assignable} annotation.

IGJ only permits a single immutability parameter, which simplifies the subtyping rule.
In contrast, types in OIGJ can have multiple immutability parameters, for example,
    \code{Iterator<O,\underline{ItrI,CollectionI},E>}.
%
Because IGJ uses a single immutability parameter,
    the immutability of an iterator and its underlying collection must be the same.
Thus, in IGJ, %
    method \code{next()} must be readonly (or you couldn't iterate over a readonly list),
    and therefore
    we had to use an \code{@Assignable} annotation on \code{ListItr.current}
    (line~\ref{OIGJ:assignable} in \Ref{Figure}{OIGJ-LinkedList}).
In contrast, in OIGJ, we guard \code{next()} with a mutable \code{ItrI} (line~\ref{I:next}),
    and guard \code{remove()} with a mutable \code{CollectionI} (line~\ref{I:remove}).
%
%
%
%


\subsection{Relationship with other work}

%
%
OIGJ uses method guards borrowed from \emph{cJ}~\cite{HuangZS2007:cJ}.
(The OIGJ implementation uses annotations syntax instead.) %

In what follows, we have room to survey only closely related papers.
%
\Ref{Figure}{Comparison} compares OIGJ to some of the previous work described below.


\textbf{Mutability and encapsulation} were first combined by
Flexible Alias Protection (FLAP)~\cite{NobleVP98}.
FLAP inspired a number of proposals including ownership
types~\cite{ClarkePN98}
and confined types~\cite{VikekB99}.
Capabilities for Sharing~\cite{BoylandNR2001}
describes the fundamentals underlying various encapsulation and
mutability approaches by separating ``mechanism'' (the semantics of
sharing and exclusion) from ``policy'' (the guarantees provided by the
resulting system). Capabilities gives a lower-level semantics that can
be enforced at compile or run time.  A reference can possess any
combination of these 7 access rights: read, write, identity
(permitting address comparisons), exclusive read, exclusive write,
exclusive identity, and ownership (giving the capability to assert
rights).  Immutability, for example, is represented by the lack of the
write right and possession of the exclusive write right.
Finally, \emph{Fractional Permissions}~\cite{BoylandRZ2009}
    can give semantics to various annotations such as unique, readonly, method effects,
    and
    an ownership variant called \emph{owner-as-effector} in which
    one cannot read or write owned state without declaring the appropriate
    effect for the owner.
%
%


\textbf{Ownership types}~\cite{ClarkeD2002,BoyapatiLR2002,BoyapatiLS2003}
    impose a structure on the references between objects in a program's memory.
OIGJ and other work~\cite{PotaninNCB2006,OstlundWC2008} enforce
    the owner-as-\emph{dominator} disciplines.
Generic Universe Types
    (\textbf{GUT})~\cite{MuellerPoetzsch-Heffter99a,DietlDM2007} enforce owner-as-\emph{modifier}
    by using three type annotations: \code{rep}, \code{peer}, and \code{readonly}.
\code{rep} denotes representation objects (similar to \This),
    while \code{peer} denotes objects owned by the same owner (similar to \hO).
\textbf{UTT}~\cite{MullerR2007} is an extension of Universe Types
    that supports ownership transfer by utilizing a modular static analysis, which is useful for merging data-structures
    or complex object initialization.
%
%

MOJO~\cite{CameronDNS2007} can express multiple ownership: objects can have more than one owner at run time.
OIGJ supports only a single \emph{owner} at run time.
(OIGJ supports multiple \emph{owner parameters}, but according to the \textbf{Ownership nesting rule},
    all owner parameters are inside the first owner parameter.)
%
%
%
%
%
%
%

Jo$\exists$~\cite{CameronD2009} supports variant subtyping over the owner parameter
    by using existential types.
OIGJ supports wildcards used as owners for stack variables, but those are less flexible than Jo$\exists$.
For example, Jo$\exists$ can distinguish a list of students that may
    have different owners, from a list of student that share the same unknown owner.

\textbf{Immutability and ownership.}
Similarly to OIGJ,
    Immutable Objects for a Java-like Language (\textbf{IOJ})~\cite{HaackPSS2007}
    associates with each type its mutability and owner.
In contrast to OIGJ, IOJ does not have generics,
    nor readonly \emph{references}. %
Moreover, in IOJ, the constructor cannot leak a reference to \this.
%
Haack and Poll~\cite{HaackPSS2007} later added flexible initialization of immutable objects,
    i.e., an immutable object may still be mutated after its constructor returns.
They use the annotations \code{RdWr}, \code{Rd}, \code{Any}, and \code{myaccess},
    which corresponds to our \code{Mutable}, \code{Immut}, \code{ReadOnly}, and \code{I}.
In addition, they have an inference algorithm that automatically infers the end of object initialization phases.
(Their algorithm infers which variables are \code{Fresh(n)}, which resembles our \code{Raw}.
    However, the programmer cannot write the \code{Fresh} annotation explicitly.)
%
%



{X10}~\cite{NystromSPG2008} supports constrained types that can refer to properties and final local variables.
%
X10 supports cyclic immutable structures by using \code{proto} annotations,
    which are similar to our immutability~\hI and the notion of cookers.
However, both X10 and IGJ cannot type-check Sun's \code{LinkedList} because an object becomes cooked when its constructor finishes.
It is possible to refactor \code{LinkedList} to fit X10's typing-rules
    by using a recursive implementation, but then you risk a stack-overflow when creating large lists.
Delayed types~\cite{FahndrichX2007}, which are similar to X10's \code{proto},
    are used to verify non-null fields or other heap-monotonic properties.

\textbf{JOE$_3$}~\cite{OstlundWC2008} combines ownership (as dominators, not modifiers),
    uniqueness, and immutability.
It also supports owner-polymorphic methods, but not existential owners.

Frozen Objects~\cite{LeinoMW2008} show how ownership can help support immutability
by allowing programmers to decide when the object should become immutable. This system
takes a verification approach rather than a simple type checker such as OIGJ. Frozen Objects show
how flexible the initialization stage can potentially be in the presence of ownership and immutability,
while OIGJ shows how much flexibility can be achieved while staying at the type checking level.

\textbf{Readonly references} are  found in \CC (using the \const{} keyword),
JAC~\cite{KnieselT2001}, modes \cite{SkoglundW2001},
Javari \cite{TschantzE2005}, etc.
Previous work on readonly references
    lack ownership information.
Boyland~\cite{Boyland2005} observes that readonly does not address
observational exposure, i.e., modifications on one side of an
abstraction boundary that are observable on the other side.
Immutable objects address such exposure because their state cannot
change.
%
%


\textbf{List iterators} pose a challenge to ownership because
    they require a direct pointer to the list's privately owned entries,
    thus breaking the owner-as-dominator property.
Both OIGJ and SafeJava~\cite{BoyapatiLS2003} allow an inner instance
    to access the outer instance's privately owned objects.
Clarke~\cite{ClarkeD2002} suggested to use iterators only with stack variables,
    i.e., you cannot store an iterator in a field.
It is also possible to redesign the code and implement iterators without violating ownership,
    e.g., by using internal iterators or magic-cookies~\cite{Noble2000}.

%
%


\vspace{-0.5cm}

\Section[conclusion]{Conclusion}
OIGJ is a Java language extension
    that supports both ownership and immutability,
    while enhancing
    the expressiveness of each individual concept.
By using Java's generic types, OIGJ simplifies previous type mechanisms,
    such as existential owners, scoped regions, and owner-polymorphic methods.
OIGJ is easy to understand and implement, using only 14 (flow-insensitive)
    typing rules beyond those of Java.
We have formalized a core calculus called FOIGJ and proved it sound.
Our implementation is backward-compatible with Java, and it scales to
realistic programs.
OIGJ can type-check Sun's \code{java.util} collections
    (without the \code{clone} method),
    using a small number of annotations.
Finally, various design patterns, such as the factory and visitor patterns, can be expressed in OIGJ,
    making it ready for practical use.
An implementation is publicly available at {\footnotesize \url{http://types.cs.washington.edu/checker-framework/}}.

Future work includes
    inferring ownership and immutability, %
    conducting a bigger case study with client and library code,
    and extending OIGJ with concepts such as
    \emph{owner-as-modifier}~\cite{ZibinEtAlOsMTR2010},
    \emph{uniqueness}, and
    \emph{external-uniqueness}~\cite{ClarkeW2003:ECOOP}.




%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%

%


\vspace{-0.3cm}

\acks

\vspace{-0.1cm}

This work was supported by the grants from RSNZ Marsden,
ISAT, and NSF CNS-0855252. We especially thank
Werner Dietl, James Noble, ELVIS, and the
anonymous referees.

\vspace{-0.1cm}

\bibliographystyle{plainnat}
\begin{thebibliography}{41}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
  \providecommand{\doi}[1]{doi: #1}\else
  \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

\footnotesize

\bibitem[Boyapati(2004)]{Boyapati2004:PhD}
Chandrasekhar Boyapati.
\newblock \emph{{SafeJava}: A Unified Type System for Safe Programming}.
\newblock PhD thesis, MIT Dept. of EECS, Feb. 2004.

\bibitem[Boyapati et~al.(2002)Boyapati, Lee, and Rinard]{BoyapatiLR2002}
Chandrasekhar Boyapati, Robert Lee, and Martin Rinard.
\newblock Ownership types for safe programming: Preventing data races and
  deadlocks.
\newblock In \emph{OOPSLA}, pages 211--230, Oct. 2002.

\bibitem[Boyapati et~al.(2003)Boyapati, Liskov, and Shrira]{BoyapatiLS2003}
Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira.
\newblock Ownership types for object encapsulation.
\newblock In \emph{POPL}, pages 213--223, Jan. 2003.

\bibitem[Boyland(2005)]{Boyland2005}
John Boyland.
\newblock Why we should not add \texttt{readonly} to {Java} (yet).
\newblock In \emph{FTfJP}, July 2005.

\bibitem[Boyland et~al.(2001)Boyland, Noble, and Retert]{BoylandNR2001}
John Boyland, James Noble, and William Retert.
\newblock Capabilities for sharing: A generalisation of uniqueness and
  read-only.
\newblock In \emph{ECOOP}, pages 2--27, June 2001.

\bibitem[Boyland et~al.(2009)Boyland, Retert, and Zhao]{BoylandRZ2009}
John Boyland, William Retert, and Yang Zhao.
\newblock Comprehending annotations on object-oriented programs using
  fractional permissions.
\newblock In \emph{IWACO}, pages 1--11, July 2009.

\bibitem[Bracha et~al.(1998)Bracha, Odersky, Stoutamire, and
  Wadler]{BrachaOSW98}
Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler.
\newblock Making the future safe for the past: Adding genericity to the {Java}
  programming language.
\newblock In \emph{OOPSLA}, pages 183--200, Oct. 1998.

\bibitem[Cameron and Drossopoulou(2009)]{CameronD2009}
Nicholas Cameron and Sophia Drossopoulou.
\newblock Existential quantification for variant ownership.
\newblock In \emph{ESOP}, pages 128--142, Mar. 2009.

\bibitem[Cameron et~al.(2008)Cameron, Drossopoulou, and Ernst]{CameronDE2008}
Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst.
\newblock A model for {Java} with wildcards.
\newblock In \emph{ECOOP}, pages 2--26, July 2008.

\bibitem[Cameron et~al.(2007)Cameron, Drossopoulou, Noble, and
  Smith]{CameronDNS2007}
Nicholas~R. Cameron, Sophia Drossopoulou, James Noble, and Matthew~J. Smith.
\newblock Multiple ownership.
\newblock In \emph{OOPSLA}, pages 441--460, Oct. 2007.

\bibitem[Clarke and Drossopoulou(2002)]{ClarkeD2002}
Dave Clarke and Sophia Drossopoulou.
\newblock Ownership, encapsulation and the disjointness of type and effect.
\newblock In \emph{OOPSLA}, pages 292--310, Oct. 2002.

\bibitem[Clarke and Wrigstad(2003)]{ClarkeW2003:ECOOP}
Dave Clarke and Tobias Wrigstad.
\newblock External uniqueness is unique enough.
\newblock In \emph{ECOOP}, pages 176--200, July 2003.

\bibitem[Clarke et~al.(1998)Clarke, Potter, and Noble]{ClarkePN98}
David~G. Clarke, John~M. Potter, and James Noble.
\newblock Ownership types for flexible alias protection.
\newblock In \emph{OOPSLA}, pages 48--64, Oct. 1998.

\bibitem[Dietl et~al.(2007)Dietl, Drossopoulou, and M{\"u}ller]{DietlDM2007}
Werner Dietl, Sophia Drossopoulou, and Peter M{\"u}ller.
\newblock {G}eneric {U}niverse {T}ypes.
\newblock In \emph{ECOOP}, pages 28--53, Aug. 2007.

\bibitem[Ernst(2008)]{JSR308-2008-09-12}
Michael~D. Ernst.
\newblock {Type Annotations} specification ({JSR} 308).
\newblock \url{http://types.cs.washington.edu/jsr308/}, Sep.~12, 2008.

\bibitem[F{\"a}hndrich and Xia(2007)]{FahndrichX2007}
Manuel F{\"a}hndrich and Songtao Xia.
\newblock Establishing object invariants with delayed types.
\newblock In \emph{OOPSLA}, pages 337--350, Oct. 2007.

\bibitem[Gamma et~al.(1995)Gamma, Helm, Johnson, and Vlissides]{designpatterns}
Erich Gamma, Richard Helm, Ralph~E. Johnson, and John Vlissides.
\newblock \emph{Design Patterns}.
\newblock Addison-Wesley, Reading, MA, 1995.

\bibitem[Haack and Poll(2009)]{HaackP2009}
Christian Haack and Erik Poll.
\newblock Type-based object immutability with flexible initialization.
\newblock In \emph{{ECOOP}}, pages 520--545, 2009.

\bibitem[Haack et~al.(2007)Haack, Poll, Sch{\"a}fer, and
  Schubert]{HaackPSS2007}
Christian Haack, Erik Poll, Jan Sch{\"a}fer, and Aleksy Schubert.
\newblock Immutable objects for a {Java}-like language.
\newblock In \emph{ESOP}, pages 347--362, Mar. 2007.

\bibitem[Huang et~al.(2007)Huang, Zook, and Smaragdakis]{HuangZS2007:cJ}
Shan~Shan Huang, David Zook, and Yannis Smaragdakis.
\newblock {cJ}: Enhancing {Java} with safe type conditions.
\newblock In \emph{AOSD}, pages 185--198, Mar. 2007.

\bibitem[Igarashi et~al.(2001)Igarashi, Pierce, and Wadler]{Igarashi:2001:FJM}
Atsushi Igarashi, Benjamin~C. Pierce, and Philip Wadler.
\newblock Featherweight {Java}: a minimal core calculus for {Java} and {GJ}.
\newblock \emph{ACM TOPLAS}, 23\penalty0 (3):\penalty0 396--450, May 2001.
\newblock ISSN 0164-0925.

\bibitem[Kniesel and Theisen(2001)]{KnieselT2001}
G{\"u}nter Kniesel and Dirk Theisen.
\newblock {JAC} --- access right based encapsulation for {Java}.
\newblock \emph{Software: Practice and Experience}, 31\penalty0 (6):\penalty0
  555--576, 2001.

\bibitem[Leino et~al.(2008)Leino, M{\"u}ller, and Wallenburg]{LeinoMW2008}
K.~Rustan~M. Leino, Peter M{\"u}ller, and Angela Wallenburg.
\newblock Flexible immutability with frozen objects.
\newblock In \emph{VSTTE}, pages 192--208, Oct. 2008.

\bibitem[M{\"u}ller and Poetzsch-Heffter(1999)]{MuellerPoetzsch-Heffter99a}
P.~M{\"u}ller and A.~Poetzsch-Heffter.
\newblock Universes: A type system for controlling representation exposure.
\newblock In \emph{Programming Languages and Fundamentals of Programming},
  pages 131--140, 1999.

\bibitem[M{\"u}ller and Rudich(2007)]{MullerR2007}
Peter M{\"u}ller and Arsenii Rudich.
\newblock Ownership transfer in universe types.
\newblock In \emph{OOPSLA}, pages 461--478, Oct. 2007.

\bibitem[N{\"a}geli(2006)]{Nageli2006}
Stefan N{\"a}geli.
\newblock Ownership in design patterns.
\newblock Master's thesis, ETH Z{\"u}rich, Z{\"u}rich, Switzerland, Mar. 2006.

\bibitem[Noble(2000)]{Noble2000}
James Noble.
\newblock Iterators and encapsulation.
\newblock In \emph{TOOLS Pacific}, pages 431--442, 2000.

\bibitem[Noble et~al.(1998)Noble, Vitek, and Potter]{NobleVP98}
James Noble, Jan Vitek, and John Potter.
\newblock Flexible alias protection.
\newblock In \emph{ECOOP}, pages 158--185, July 1998.

\bibitem[Nystrom et~al.(2008)Nystrom, Saraswat, Palsberg, and
  Grothoff]{NystromSPG2008}
Nathaniel Nystrom, Vijay Saraswat, Jens Palsberg, and Christian Grothoff.
\newblock Constrained types for object-oriented languages.
\newblock In \emph{OOPSLA}, pages 457--474, Oct. 2008.

\bibitem[{\"O}stlund et~al.(2008){\"O}stlund, Wrigstad, and
  Clarke]{OstlundWC2008}
Johan {\"O}stlund, Tobias Wrigstad, and Dave Clarke.
\newblock Ownership, uniqueness and immutability.
\newblock In \emph{Tools Europe}, pages 178--197, 2008.

\bibitem[Papi et~al.(2008)Papi, Ali, {Correa~Jr.}, Perkins, and
  Ernst]{PapiACPE2008}
Matthew~M. Papi, Mahmood Ali, Telmo~Luis {Correa~Jr.}, Jeff~H. Perkins, and
  Michael~D. Ernst.
\newblock Practical pluggable types for {Java}.
\newblock In \emph{ISSTA}, pages 201--212, July 2008.

\bibitem[Pierce(2002)]{pierce:2002:types-and-pls}
Benjamin~C. Pierce.
\newblock \emph{Types and Programming Languages}.
\newblock MIT Press, 2002.

\bibitem[Potanin et~al.(2006)Potanin, Noble, Clarke, and
  Biddle]{PotaninNCB2006}
Alex Potanin, James Noble, Dave Clarke, and Robert Biddle.
\newblock {Generic} {Ownership} for {Generic} {Java}.
\newblock In \emph{OOPSLA}, pages 311--324, Oct. 2006.

\bibitem[Skoglund and Wrigstad(2001)]{SkoglundW2001}
Mats Skoglund and Tobias Wrigstad.
\newblock A mode system for read-only references in {Java}.
\newblock In \emph{FTfJP}, June 2001.

\bibitem[Tschantz and Ernst(2005)]{TschantzE2005}
Matthew~S. Tschantz and Michael~D. Ernst.
\newblock Javari: Adding reference immutability to {Java}.
\newblock In \emph{OOPSLA}, pages 211--230, Oct. 2005.

\bibitem[Vitek and Bokowski(1999)]{VikekB99}
Jan Vitek and Boris Bokowski.
\newblock Confined types.
\newblock In \emph{OOPSLA}, pages 82--96, Nov. 1999.

\bibitem[Wrigstad(2006)]{Wrigstad2006}
Tobias Wrigstad.
\newblock \emph{Ownership-Based Alias Management}.
\newblock PhD thesis, Royal Institute of Technology, Sweden, May 2006.

\bibitem[Wrigstad and Clarke.(2007)]{WrigstadC2007}
Tobias Wrigstad and Dave Clarke.
\newblock Existential owners for ownership types.
\newblock \emph{J. Object Tech.}, 6\penalty0 (4):\penalty0 141--159, May--June
  2007.

\bibitem[Zibin(2010)]{ZibinUpdated2010}
Yoav Zibin.
\newblock {F}eatherweight {O}wnership and {I}mmutability {G}eneric {J}ava
  {(FOIGJ)}.
\newblock Technical Report 10-16, ECS, VUW, June 2010.
\newblock \url{http://ecs.victoria.ac.nz/Main/TechnicalReportSeries}.

\bibitem[Zibin et~al.(2007)Zibin, Potanin, Ali, Artzi, Kie{\.z}un, and
  Ernst]{ZibinPAAKE2007}
Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kie{\.z}un, and
  Michael~D. Ernst.
\newblock Object and reference immutability using {Java} generics.
\newblock In \emph{ESEC/FSE}, pages 75--84, Sep. 2007.

\bibitem[Zibin et~al.(2010)Zibin, Potanin, Li, Ali, and
  Ernst]{ZibinEtAlOsMTR2010}
Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael~D. Ernst.
\newblock {OIGJ} with owners as modifiers.
\newblock Technical Report 10-15, ECS, VUW, January 2010.

\end{thebibliography}


\label{ignore-label-for-etags}

\end{document}
